% TT1 prove (({x} (~p(x) v r(x))) => (p(a) => r(a))). % TT2 prove ~~( ({y} (p(x) v ~p(y)))). % TT4 prove ((p(a) & r(a) & ({x} (~r(x) v r(f(x)))) & ({x} (~p(x) v p(f(x)))) & ({x} (~r(x) v ~p(x) v s(x))) & ({x} (~s(x) v ~p(x) v ~r(x) v n(f(x))))) => (n(f(f(a))) & n(f(f(a))))). % TT3 prove ((p(a) & ({x} (~p(x) v p(f(x))))) => (p(f(a)) & p(f(a)))). % NP1 refute (({x} (p(x) v q(c))) => (q(c) v ({x} p(x)))). % NP2 refute ((a(0) => ( b(x))) => ( (a(0) => b(x)))). % NP3 refute (~({x} a(x)) => ( ~a(x))). % NP4 refute ((({x} a(x)) => b(0)) => ( (a(x) => b(0)))). % I1 prove (({x} ({y} (p(x) & r(y)))) => ({u} ({v} (p(v) & r(u))))). % I1Y prove ((({x} ({y} (p(x) & r(y)))) => ({u} ({v} (p(u) & r(v))))) & (s(a) => s(a))). % I1.1 prove ((({x} p(x)) & ({y} r(y))) => ({u} ({v} (p(v) & r(u))))). % T1 prove (({x} ({y} (p(x) & r(y)))) => ({u} ({v} (p(v) & r(u))))). % T1A prove (({x} ({y} p(x))) => ({u} ({v} p(v)))). % T1B prove (({x} ({y} (p(x) & r(y)))) => ({u} ({v} p(v)))). % T1C prove (({x} (p(x) & r(a))) => p(b)). % T2 prove (p(a) => p(a)). % T3 prove (p(a) => (p(a) v p(b))). % T4 prove (({x} ( ({z} ( ({u} (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u)))))))). % T4S prove (({x} ({z} ({u} (p(x) & q(y(x)) & r(z) & s(w(x,z)) & t(u))))) => ({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u)))))))). % T4S.1 prove ((({x} p(x)) & ({x} q(y(x))) & ({z} r(z)) & ({x} s(w(x,z))) & ({x} t(x))) => ({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u)))))))). % T5 prove (({x} ( ({z} (p(x) & q(y) & r(z))))) => ({z} ( ({x} (p(x) & q(y) & r(z)))))). % T6 prove ((p(a) v p(b)) => ( p(x))). % T7 prove (({x} ( ({z} (p(x) & q(y) & r(z))))) => ({z} ( ({x} (p(x) & q(y) & r(z)))))). % T8 prove (( ({x} (p(x) & q(y)))) => ( ({x} (p(x) & q(y))))). % T9 prove (( ({y} p(x,y))) => ( ({y} p(x,y)))). % THARD prove ((({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xb} ({xa} ((inh(xa) & inh(xb)) => inh(and(xa,xb))))) & ({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & ((inh(xb) => inh(xc)) & inh(or(xa,xb)))) => inh(xc)))))) => ({xc} ({xb} (inh(or(xb,xc)) => inh(or(and(xb,xb),xc)))))). % SICS1.1 prove ((({x} ( ({z} (p(x) & q(y) & r(z))))) => ({z1} ( ({x1} (p(x1) & q(y1) & r(z1)))))) & (({z2} ( ({x2} (p(x2) & q(y2) & r(z2))))) => ({x3} ( ({z3} (p(x3) & q(y3) & r(z3))))))). % SICS1.1-1 prove (({x} ( ({z} (p(x) & q(y) & r(z))))) => ({z1} ( ({x1} (p(x1) & q(y1) & r(z1)))))). % SICS1.1-2 prove (({z} ( ({x} (p(x) & q(y) & r(z))))) => ({x1} ( ({z1} (p(x1) & q(y1) & r(z1)))))). % SICS1.1-3 prove ((({x} ( ({z} (p1(x) & q1(y) & r1(z))))) => ({z1} ( ({x1} (p1(x1) & q1(y1) & r1(z1)))))) & (({z2} ( ({x2} (p(x2) & q(y2) & r(z2))))) => ({x3} ( ({z3} (p(x3) & q(y3) & r(z3))))))). % SICS1.2 prove ((({x} ( ({z} ( (p(x) & q(y) & r(z) & s(w)))))) => ( ({z2} ( ({x2} (p(x2) & q(y2) & r(z2) & s(w2))))))) & (( ({z1} ( ({x1} (p(x1) & q(y1) & r(z1) & s(w1)))))) => ({x3} ( ({z3} ( (p(x3) & q(y3) & r(z3) & s(w3)))))))). % SICS1.2-1 prove (({z} ( (r(z) & s(w)))) => ( ({x2} (r(x2) & s(w2))))). % SICS1.2-1A prove (({x} ( ({z} ( (p(x) & q(y) & r(z) & s(w)))))) => ( ( ( ( (p(x1) & q(y1) & r(z1) & s(w1))))))). % SICS1.2-2 prove (( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w)))))) => ({x} ( ({z} ( (p(x) & q(y) & r(z) & s(w))))))). % SICS1.3 prove ((({x} ( ({z} ( ({u} (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u)))))))) & (({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ({x} ( ({z} ( ({u} (p(x) & q(y) & r(z) & s(w) & t(u))))))))). % SICS1.3-X prove ((({x} ( ({z} ( ({u} (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ({u1} ( ({z1} ( ({x1} (p(x1) & q(y1) & r(z1) & s(w1) & t(u1)))))))) & (({u2} ( ({z2} ( ({x2} (p(x2) & q(y2) & r(z2) & s(w2) & t(u2))))))) => ({x3} ( ({z3} ( ({u3} (p(x3) & q(y3) & r(z3) & s(w3) & t(u3))))))))). % SICS1.3-1 prove (({x} ( ({z} ( ({u} (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u)))))))). % SICS1.3-2 prove (({u} ( ({z} ( ({x} (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ({x} ( ({z} ( ({u} (p(x) & q(y) & r(z) & s(w) & t(u)))))))). % SICS1.4 prove ((( ({x} ( (p(x) & q(y) & r(z))))) => ( ({x} ( (p(x) & q(y) & r(z)))))) & (( ({x} ( (p(x) & q(y) & r(z))))) => ( ({x} ( (p(x) & q(y) & r(z))))))). % SICS1.4-1 prove (( ({x} ( (p(x) & q(y) & r(z))))) => ( ({x} ( (p(x) & q(y) & r(z)))))). % SICS1.4-2 prove (( ({x} ( (p(x) & q(y) & r(z))))) => ( ({x} ( (p(x) & q(y) & r(z)))))). % SICS1.5 prove ((( ({x} ( ({w} (p(x) & q(y) & r(z) & s(w)))))) => ({w} ( ({x} ( (p(x) & q(y) & r(z) & s(w))))))) & (({w} ( ({x} ( (p(x) & q(y) & r(z) & s(w)))))) => ( ({x} ( ({w} (p(x) & q(y) & r(z) & s(w)))))))). % SICS1.5-1 prove (( ({x} ( ({w} (p(x) & q(y) & r(z) & s(w)))))) => ({w} ( ({x} ( (p(x) & q(y) & r(z) & s(w))))))). % SICS1.5-2 prove (({w} ( ({x} ( (p(x) & q(y) & r(z) & s(w)))))) => ( ({x} ( ({w} (p(x) & q(y) & r(z) & s(w))))))). % SICS1.6 prove ((( ({x} ( ({w} ( (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ( ({w2} ( ({x2} ( (p(x2) & q(y2) & r(z2) & s(w2) & t(u2)))))))) & (( ({w1} ( ({x1} ( (p(x1) & q(y1) & r(z1) & s(w1) & t(u1))))))) => ( ({x3} ( ({w3} ( (p(x3) & q(y3) & r(z3) & s(w3) & t(u3))))))))). % SICS1.6-1 prove (( ({x} ( ({w} ( (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ( ({w} ( ({x} ( (p(x) & q(y) & r(z) & s(w) & t(u)))))))). % SICS1.6-2 prove (( ({w} ( ({x} ( (p(x) & q(y) & r(z) & s(w) & t(u))))))) => ( ({x1} ( ({w1} ( (p(x1) & q(y1) & r(z1) & s(w1) & t(u1)))))))). % SICS1.7 prove (( ({y1} ( ({y2} (p(x1,y1) & q(x2,y2)))))) => ({y2} ( ({y1} ( (p(x1,y1) & q(x2,y2))))))). % SICS1.8 prove (( ({y1} ( ({y2} ( ({y3} (p(x1,y1) & q(x2,y2) & r(x3,y3)))))))) => ({y3} ( ({y2} ( ({y1} ( (p(x1,y1) & q(x2,y2) & r(x3,y3))))))))). % SICS2.1 prove ((({x} a(nil,x,x)) & ({x} ({y} ({z} ({w} (a(y,z,w) => a(c(x,y),z,c(x,w)))))))) => ( a(c(a1,c(a2,c(a3,c(a4,c(a5,nil))))),nil,x))). % SICS2.1-X prove ((({x1} a(nil,x1,x1)) & ({x} ({y} ({z} ({w} (a(y,z,w) => a(c(x,y),z,c(x,w)))))))) => ( a(c(a1,nil),nil,x2))). % SICS2.1-X2 prove ((({x1} a(nil,x1,x1)) & ({x} ({y} ({z} ({w} (a(y,z,w) => a(c(x,y),z,c(x,w)))))))) => ( a(c(a2,c(a1,nil)),nil,x2))). % SICS2.1-X3 prove ((a(nil) & ({y} (a(y) => a(c(y))))) => a(c(c(nil)))). % SICS2.1-Y prove ((({z} p(a1)) & ({x} (p(a1) => p(c(x))))) => ( p(c(c(y))))). % SICS2.1-Z prove ((({z} p(a)) & ({x} (p(a) => p(b)))) => p(b)). % SICS2.1-ZS prove ((p(a) & (~p(a) v p(b))) => ( p(b))). % SICS2.1-ZS1 prove (p(a) => ( p(a))). % SICS2.2 prove ((({x} a(nil,x,x)) & ({x} ({y} ({z} ({w} (a(y,z,w) => a(c(x,y),z,c(x,w)))))))) => ( a(c(a1,c(a2,c(a3,c(a4,c(a5,c(a6,nil)))))),nil,x))). % SICS2.3 prove ((({x1} a(nil,x1,x1)) & ({x} ({y} ({z} ({w} (a(y,z,w) => a(c(x,y),z,c(x,w)))))))) => ( a(c(a1,c(a2,c(a3,c(a4,c(a5,c(a6,c(a7,nil))))))),nil,x2))). % SICS2.4 prove ((({x1} a(nil,x1,x1)) & ({x} ({y} ({z} ({w} (a(y,z,w) => a(c(x,y),z,c(x,w)))))))) => ( a(c(a1,c(a2,c(a3,c(a4,c(a5,c(a6,c(a7,c(a8,nil)))))))),nil,x2))). % SICS2.4.1 prove ((a(nil,x,x) & ({x} ({y} (~a(y,z,w) v a(c(x,y),z,c(x,w)))))) => ( a(c(a1,c(a2,c(a3,c(a4,c(a5,c(a6,c(a7,c(a8,nil)))))))),nil,x))). % SICS3.1 prove ~( ({y} ((m(y,x) => ~m(x,x)) & (~m(x,x) => m(y,x))))). % SICS3.2 prove (( ({y} ((m(x,y) => m(x,x)) & (m(x,x) => m(x,y))))) => ~({x} ( ({z} ((m(z,y) => ~m(z,x)) & (~m(z,x) => m(z,y))))))). % SICS3.3 prove (({z} ( ({x} ((m(x,y) => (m(x,z) & ~m(x,x))) & ((m(x,z) & ~m(x,x)) => m(x,y)))))) => ~( ({y} m(y,x)))). % SICS3.3-1 prove (({z} ({x} ((m(x,y(z)) => (m(x,z) & ~m(x,x))) & ((m(x,z) & ~m(x,x)) => m(x,y(z)))))) => ~( ({y} m(y,x)))). % SICS3.4 prove ~( ({y} ((m(y,x) => ~( (m(x,w) & m(w,x)))) & (~( (m(x,w) & m(w,x))) => m(y,x))))). % SICS3.5 prove (({x} ({y} ((e(x,y) => ({z} ((m(z,x) => m(z,y)) & (m(z,y) => m(z,x))))) & (({z} ((m(z,x) => m(z,y)) & (m(z,y) => m(z,x)))) => e(x,y))))) => ({x} ({y} (e(x,y) => e(y,x))))). % SICS4.X prove ((({x} (p(x) => (p(h(x)) v p(g(x))))) & ( p(x)) & ({x} ~p(h(x)))) => ( p(g(x)))). % SICS4.Y prove (((p(a) => (p(b) v p(c))) & p(a) & ~p(b)) => p(c)). % SICS4.Z prove (((p(b) v p(c)) & ~p(b)) => p(c)). % SICS4.1 prove ((({x} (p(x) => (p(h(x)) v p(g(x))))) & ( p(x)) & ({x} ~p(h(x)))) => ( p(g(g(g(g(g(x)))))))). % SICS4.2 prove ((({x} (p(x) => (p(h(x)) v p(g(x))))) & ( p(x)) & ({x} ~p(h(x)))) => ( p(g(g(g(g(g(g(x))))))))). % SICS4.3 prove ((({x} (p(x) => (p(h(x)) v p(g(x))))) & ( p(x)) & ({x} ~p(h(x)))) => ( p(g(g(g(g(g(g(g(x)))))))))). % SICS5.0 prove ({x0} ( ((p(x1) => p(f(x0,x0))) & (p(f(x0,x0)) => p(x1))))). % SICS5.1 prove ({x0} ( ( ( ( ( ((p(x1,x2,x3,x4,x5) => p(f(x0,x0),f(x1,x1),f(x2,x2),f(x3,x3),f(x4,x4))) & (p(f(x0,x0),f(x1,x1),f(x2,x2),f(x3,x3),f(x4,x4)) => p(x1,x2,x3,x4,x5))))))))). % SICS5.2 prove ({x0} ( ( ( ( ( ( ( ( ( ( ((p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) => p(f(x0,x0),f(x1,x1),f(x2,x2),f(x3,x3),f(x4,x4),f(x5,x5),f(x6,x6),f(x7,x7),f(x8,x8),f(x9,x9))) & (p(f(x0,x0),f(x1,x1),f(x2,x2),f(x3,x3),f(x4,x4),f(x5,x5),f(x6,x6),f(x7,x7),f(x8,x8),f(x9,x9)) => p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)))))))))))))). % SICS5.3 prove ({x0} ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ((p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) => p(f(x0,x0),f(x1,x1),f(x2,x2),f(x3,x3),f(x4,x4),f(x5,x5),f(x6,x6),f(x7,x7),f(x8,x8),f(x9,x9),f(x10,x10),f(x11,x11),f(x12,x12),f(x13,x13),f(x14,x14))) & (p(f(x0,x0),f(x1,x1),f(x2,x2),f(x3,x3),f(x4,x4),f(x5,x5),f(x6,x6),f(x7,x7),f(x8,x8),f(x9,x9),f(x10,x10),f(x11,x11),f(x12,x12),f(x13,x13),f(x14,x14)) => p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15))))))))))))))))))). % SICS6.1 prove ((({x} ({y} (p(x) => q(y)))) => (( p(x)) => ({y} q(y)))) & ((( p(x)) => ({y} q(y))) => ({x} ({y} (p(x) => q(y)))))). % SICS6.2 prove ((~( ( ( ( ( ( ( ( ( ( p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10))))))))))) => ({x1} ({x2} ({x3} ({x4} ({x5} ({x6} ({x7} ({x8} ({x9} ({x10} ~p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)))))))))))) & (({x1} ({x2} ({x3} ({x4} ({x5} ({x6} ({x7} ({x8} ({x9} ({x10} ~p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10))))))))))) => ~( ( ( ( ( ( ( ( ( ( p(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10))))))))))))). % SICS6.3 prove ((( (p(x) & ({y} (q(y) => r(x,y))))) & ~( (q(x) & ({y} (p(y) => r(x,y)))))) => ~({x} (p(x) => q(x)))). % SICS6.4 prove (({x} ((p(x) => ( (q(y) & r(x,y)))) & (( (q(y1) & r(x,y1))) => p(x)))) => ({x1} ((~p(x1) => ({y2} ~(q(y2) & r(x1,y2)))) & (({y3} ~(q(y3) & r(x1,y3))) => ~p(x1))))). % SICS6.5 prove ((({x} ((p(x) => q(x)) & (q(x) => p(x)))) & ({x} ((r(x) => s(x)) & (s(x) => r(x))))) => ({x} (((p(x) & ~r(x)) => (q(x) & ~s(x))) & ((q(x) & ~s(x)) => (p(x) & ~r(x)))))). % SICS6.6 prove ((({x} (p(x) => q(x))) & ({x} (q(x) => s(x)))) => ({x} (~~p(x) => ~~s(x)))). % SICS6.7 prove ((( p(x)) & ({x} ({y} ((p(y) & q(x)) => ~r(x))))) => ({x} ((q(x) & r(x)) => s(x)))). % SICS6.8 prove ((({x} (p(x) => ( (q(x,y) & r(y))))) & ( ( (q(x,y) v p(x))))) => ( ( q(x,y)))). % SICS6.9 prove ((({x} (p(x) => (r(x) v ( q(x,y))))) & ({x} (r(x) => ~( p(x)))) & ( p(x))) => ( ( q(x,y)))). % SICS6.10 prove ((( (p(x) & ({y} (q(y) => (r(x,y) v r(y,x)))))) & ( (q(x1) & ({y1} (p(y1) => ~r(x1,y1)))))) => ( ( (p(x2) & q(y2) & r(x2,y2))))). % SICS6.11 prove ((~( ({y} (q(y) => r(x,y)))) & ( ({y} (s(y) => r(x,y))))) => ~({x} (q(x) => s(x)))). % SICS6.12 prove ((p(a) & ~p(f(f(f(f(f(a))))))) => ~~( (p(x) & ~p(f(x))))). % SICS6.13 prove ((({x} ((p(x) => (q(x) v r(x) v ( s(x,y)))) & ((q(x) v r(x) v ( s(x,y5))) => p(x)))) & ( ( (s(y1,x1) v g(x1)))) & ({x2} ((g(x2) => (( s(x2,y2)) v ( (r(z2) v q(z2) v s(a,z2))))) & ((( s(x2,y3)) v ( (r(z) v q(z) v s(a,z)))) => g(x2))))) => (( q(x3)) v ( r(x4)) v ( ( s(x5,y4))))). % SICS6.14 prove ((({x1} ({x2} ( ( (p(x1) & q(x2) & r(y1) & s(y2)))))) => ( ( ({x1} ({x2} (p(x1) & q(x2) & r(y1) & s(y2))))))) & (( ( ({x1} ({x2} (p(x1) & q(x2) & r(y1) & s(y2)))))) => ({x1} ({x2} ( ( (p(x1) & q(x2) & r(y1) & s(y2)))))))). % SICS6.14-1 prove (({x1} ({x2} ( ( (p(x1) & q(x2) & r(y1) & s(y2)))))) => ( ( ({x1} ({x2} (p(x1) & q(x2) & r(y1) & s(y2))))))). % SICS6.14-2 prove (( ( ({x1} ({x2} (p(x1) & q(x2) & r(y1) & s(y2)))))) => ({x1} ({x2} ( ( (p(x1) & q(x2) & r(y1) & s(y2))))))). % SICS6.15 prove ((({x} (p(x) => ~( (q(y) & r(x,y))))) & ({x} (t(x) => ( (s(y) & r(x,y))))) & ({x} (p(x) => ~~t(x))) & ({y} (s(y) => q(y)))) => ~( p(x))). % SICS7.0-1 prove (q(a1,a2,a1,a2) => ((((p(a1) & p(a2)) => (p(a1) & p(a2))) & ((p(a1) & p(a2)) => (p(a1) & p(a2)))) & q(a1,a2,a1,a2))). % SICS7.0-2 prove (q(a1,a2,a1,a2) => ( ( ( ( (((p(y1) & p(y2)) => (p(x1) & p(x2))) & q(x1,x2,y1,y2))))))). % SICS7.0-3 prove (q(a1,a2,a1,a2) => ( ( ( ( (((p(b) & p(b)) => (p(b) & p(b))) & q(x1,x2,y1,y2))))))). % SICS7.0-4 prove (q(a) => ( (((p(b) & p(b)) => (p(b) & p(b))) & q(a)))). % SICS7.0-5 prove (q(a) => (((p(b) & p(b)) => (p(b) & p(b))) & q(a))). % SICS7.0-6 prove (q(a) => ((p(b) & p(b)) => (p(b) & p(b)))). % SICS7.0-7 prove ((p(b) & p(b)) => (p(b) & p(b))). % SICS7.0-8 prove ( ((p(b) & p(b)) => (p(b) & p(b)))). % SICS7.0-9 prove (q(a1,a2,a1,a2) => ( ( ( ( ((((p(a1) & p(a2)) => (p(a1) & p(a2))) & ((p(a1) & p(a2)) => (p(a1) & p(a2)))) & q(a1,a2,a1,a2))))))). % SICS7.0-10 prove (q(a1,a2,a1,a2) => ( (((p(a1) & p(a2)) => (p(a1) & p(a2))) & ((p(a1) & p(a2)) => (p(a1) & p(a2)))))). % SICS7.0-11 prove ( (((p(a1) & p(a2)) => (p(a1) & p(a2))) & ((p(a1) & p(a2)) => (p(a1) & p(a2))))). % SICS7.0-12 prove ( (((p(a1) & p(a2)) => p(a1)) & ((p(a1) & p(a2)) => p(a1)))). % SICS7.0-13 prove (q(a) => (((p(a1) & p(a2)) => (p(a1) & p(a2))) & ((p(a1) & p(a2)) => (p(a1) & p(a2))))). % SICS7.0-14 prove (q(a) => ((p(a1) => p(a1)) & (p(a2) => p(a2)))). % SICS7.1 prove (q(a1,a2,a1,a2) => ( ( ( ( ((((p(x1) & p(x2)) => (p(y1) & p(y2))) & ((p(y1) & p(y2)) => (p(x1) & p(x2)))) & q(x1,x2,y1,y2))))))). % SICS7.1.1 prove (q(a1,a2,a1,a2) => ( ( ( ( ((((p(x1) & p(x2)) => (p(y1) & p(y2))) & ((p(y1) & p(y2)) => (p(x1) & p(x2)))) & q(x1,x2,y1,y2))))))). % SICS7.2 prove (q(a1,a2,a3,a1,a2,a3) => ( ( ( ( ( ( ((((p(x1) & p(x2) & p(x3)) => (p(y1) & p(y2) & p(y3))) & ((p(y1) & p(y2) & p(y3)) => (p(x1) & p(x2) & p(x3)))) & q(x1,x2,x3,y1,y2,y3))))))))). % SICS7.2-1 prove (q(a1,a2,a3,a1,a2,a3) => ( ( ( ( ( ( ((((p(x1) & (p(x2) & p(x3))) => (p(y1) & (p(y2) & p(y3)))) & ((p(y1) & (p(y2) & p(y3))) => (p(x1) & (p(x2) & p(x3))))) & q(x1,x2,x3,y1,y2,y3))))))))). % SICS7.2-1T prove (q(a1,a2,a3,a1,a2,a3) => ( ( ( ( ( ( ((((p(x1) & p(x2) & p(x3)) => (p(y1) & (p(y2) & p(y3)))) & ((p1(y1) & p1(y2) & p1(y3)) => (p1(x1) & (p1(x2) & p1(x3))))) & q(x1,x2,x3,y1,y2,y3))))))))). % SICS7.2-2 prove (q(a1,a2,a3,a1,a2,a3) => ( ( ( ( ( ( ((((p(x1) & (p(x2) & p(x3))) => (p(y1) & p(y2) & p(y3))) & ((p(y1) & (p(y2) & p(y3))) => (p(x1) & p(x2) & p(x3)))) & q(x1,x2,x3,y1,y2,y3))))))))). % TT1 prove ((p(a1) & p(a2) & p(a3)) => (p(a1) & (p(a2) & p(a3)))). % SICS7.2-3 prove (q(a1,a2,a3,a1,a2,a3) => ( ( ( ( ( ( ((((p(x1) & p(x2) & p(x3)) => (p(y1) & p(y2) & p(y3))) & ((p(y1) & p(y2) & p(y3)) => (p(x1) & p(x2) & p(x3)))) & q(x1,x2,x3,y1,y2,y3))))))))). % SICS7.3 prove (q(a1,a2,a3,a4,a1,a2,a3,a4) => ( ( ( ( ( ( ( ( ((((p(x1) & p(x2) & p(x3) & p(x4)) => (p(y1) & p(y2) & p(y3) & p(y4))) & ((p(y1) & p(y2) & p(y3) & p(y4)) => (p(x1) & p(x2) & p(x3) & p(x4)))) & q(x1,x2,x3,x4,y1,y2,y3,y4))))))))))). % SICS7.3-1 prove (q(a1,a2,a3,a4,a1,a2,a3,a4) => ( ( ( ( ( ( ( ( ((((p(x1) & (p(x2) & (p(x3) & p(x4)))) => (p(y1) & (p(y2) & (p(y3) & p(y4))))) & ((p(y1) & (p(y2) & (p(y3) & p(y4)))) => (p(x1) & (p(x2) & (p(x3) & p(x4)))))) & q(x1,x2,x3,x4,y1,y2,y3,y4))))))))))). % SICS7.4 prove (q(a1,a2,a3,a4,a5,a1,a2,a3,a4,a5) => ( ( ( ( ( ( ( ( ( ( ((((p(x1) & p(x2) & p(x3) & p(x4) & p(x5)) => (p(y1) & p(y2) & p(y3) & p(y4) & p(y5))) & ((p(y1) & p(y2) & p(y3) & p(y4) & p(y5)) => (p(x1) & p(x2) & p(x3) & p(x4) & p(x5)))) & q(x1,x2,x3,x4,x5,y1,y2,y3,y4,y5))))))))))))). % SICS7.4-1 prove (q(a1,a2,a3,a4,a5,a1,a2,a3,a4,a5) => ( ( ( ( ( ( ( ( ( ( ((((p(x1) & (p(x2) & (p(x3) & (p(x4) & p(x5))))) => (p(y1) & (p(y2) & (p(y3) & (p(y4) & p(y5)))))) & ((p(y1) & (p(y2) & (p(y3) & (p(y4) & p(y5))))) => (p(x1) & (p(x2) & (p(x3) & (p(x4) & p(x5))))))) & q(x1,x2,x3,x4,x5,y1,y2,y3,y4,y5))))))))))))). % SICS7.4-2 prove (q(a1,a2,a3,a4,a5,a1,a2,a3,a4,a5) => ( ( ( ( ( ( ( ( ( ( ((((p(x1) & p(x2) & p(x3) & p(x4) & p(x5)) => (p(y1) & (p(y2) & (p(y3) & (p(y4) & p(y5)))))) & ((p(y1) & p(y2) & p(y3) & p(y4) & p(y5)) => (p(x1) & (p(x2) & (p(x3) & (p(x4) & p(x5))))))) & q(x1,x2,x3,x4,x5,y1,y2,y3,y4,y5))))))))))))). % CL284A prove ((({x} p(a,x,x)) & ({x} p(x,a,x)) & ({x} p(x,x,a)) & p(b,c,d) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & p(y,z,v) & p(x,v,w)) => p(u,z,w)))))))) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & p(y,z,v) & p(u,z,w)) => p(x,v,w))))))))) => p(c,b,d)). % CL284A-1 prove ((({x} p(a,x,x)) & (({x} p(x,a,x)) & (({x} p(x,x,a)) & (({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & (p(y,z,v) & p(x,v,w))) => p(u,z,w)))))))) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & (p(y,z,v) & p(u,z,w))) => p(x,v,w)))))))))))) => ({x} ({y} ({u} (p(x,y,u) => p(y,x,u)))))). % CL284A-2 prove ((({x} p(a,x,x)) & ({x} p(x,a,x)) & ({x} p(x,x,a)) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & p(y,z,v) & p(x,v,w)) => p(u,z,w)))))))) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & p(y,z,v) & p(u,z,w)) => p(x,v,w))))))))) => ({x} ({y} ({u} (p(x,y,u) => p(y,x,u)))))). % CL284A-3 prove ((p(a,x,x) & ({x} p(x,a,x)) & ({x} p(x,x,a)) & ({u} ({x} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(x,v,w) v p(u,z,w))))) & ({x} ({u} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(u,z,w) v p(x,v,w)))))) => ({x} ({y} ({u} (p(x,y,u) => p(y,x,u)))))). % CL284A-4 prove ((p(a,x,x) & ({x} p(x,a,x)) & ({x} p(x,x,a)) & p(b,c,d) & ({u} ({x} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(x,v,w) v p(u,z,w))))) & ({x} ({u} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(u,z,w) v p(x,v,w)))))) => ( p(c,b,d))). % CL283 prove ((({x} p(g(x,y),x,y)) & ({x} p(x,h(x,y),y)) & ({u} ({x} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(x,v,w) v p(u,z,w))))) & ({x} ({u} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(u,z,w) v p(x,v,w)))))) => ( p(k(x),x,k(x)))). % CL284A-5 prove ((p(a,x,x) & ({x} p(x,a,x)) & ({x} p(x,x,a)) & p(b,c,d) & ({u} ({x} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(x,v,w) v p(u,z,w))))) & ({x} ({u} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(u,z,w) v p(x,v,w)))))) => ((({x} p(a,x,x)) & ({x} p(x,a,x)) & ({x} p(x,x,a)) & p(b,c,d)) => p(c,b,d))). % CL284B prove ((({x} p(a,x,x)) & ({x} p(i(x),x,a)) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & p(y,z,v) & p(x,v,w)) => p(u,z,w)))))))) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & p(y,z,v) & p(u,z,w)) => p(x,v,w))))))))) => p(b,a,b)). % CL284B-1 prove ((({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & (p(y,z,v) & p(x,v,w))) => p(u,z,w)))))))) & ({x} ({y} ({u} ({z} ({v} ({w} ((p(x,y,u) & (p(y,z,v) & p(u,z,w))) => p(x,v,w))))))))) => ({xa} ({xb} ((({x} p(xa,x,x)) & ({x} p(i(x),x,xa))) => p(xb,xa,xb))))). % CL284B-5 prove ((p(a,x,x) & ({x} p(i(x),x,a)) & ~p(b,a,b) & ({u} ({x} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(x,v,w) v p(u,z,w))))) & ({x} ({u} ({y} (~p(x,y,u) v ~p(y,z,v) v ~p(u,z,w) v p(x,v,w)))))) => nil). % INH1 prove ((({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xb} ({xa} ((inh(xa) & inh(xb)) => inh(and(xa,xb)))))) => ({xc} ({xb} ({xa} (inh(and(xa,or(xb,xc))) => inh(or(and(xa,xb),and(xa,xc)))))))). % INH2 prove ((({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xc} ({xb} ({xa} ((inh(xa) => inh(xc)) => ((inh(xb) => inh(xc)) => (inh(or(xa,xb)) => inh(xc))))))) & ({xb} ({xa} (inh(xa) => (inh(xb) => inh(and(xa,xb))))))) => ({xc} ({xb} (inh(or(xb,xc)) => inh(or(and(xb,xb),xc)))))). % INH2-M prove ((({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xc} ({xb} ({xa} ((inh(xa) => inh(xc)) => ((inh(xb) => inh(xc)) => (inh(or(xa,xb)) => inh(xc))))))) & ({xa} ({xb} (inh(and(xa,xb)) => inh(xa)))) & ({xa} ({xb} (inh(and(xa,xb)) => inh(xb)))) & ({xb} ({xa} (inh(xa) => (inh(xb) => inh(and(xa,xb))))))) => ({xc} ({xb} (inh(or(xb,xc)) => inh(or(and(xb,xb),xc)))))). % INH2-1 prove ((({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & ((inh(xb) => inh(xc)) & inh(or(xa,xb)))) => inh(xc))))) & ({xb} ({xa} ((inh(xa) & inh(xb)) => inh(and(xa,xb))))) & inh(or(b,c))) => inh(or(and(b,b),c))). % INH2-1X prove ((({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) & ({xb} ({xa} ((inh(xa) & inh(xb)) => inh(and(xa,xb)))))) => ({xb} ({xc} (inh(or(xb,xc)) => inh(or(and(xb,xb),xc)))))). % INH2-2 prove ((({xa} ({xb} (~inh(xb) v inh(or(xa,xb))))) & ({xa} (~inh(xa) v inh(or(xa,xb)))) & ({xa} ({xb} (~inh(xa) v ~inh(xb) v inh(and(xa,xb))))) & inh(or(b,c))) => (({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) => inh(or(and(b,b),c)))). % INH2-TEST prove ((({x} (~inh(x) v inh(or(and(x,x),y)))) & ({xa} ({xb} (~inh(xb) v inh(or(xa,xb))))) & inh(or(a,b))) => (({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) => inh(or(and(a,a),b)))). % INH3 prove ((({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) & ({xb} ({xa} (inh(xb) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(xa) => inh(or(xa,xb))))) & ({xb} ({xa} (inh(and(xa,xb)) => inh(xb)))) & ({xb} ({xa} (inh(and(xa,xb)) => inh(xa)))) & ({xb} ({xa} ((inh(xa) & inh(xb)) => inh(and(xa,xb)))))) => ({xc} ({xb} ({xa} (inh(and(xa,or(xb,xc))) => inh(or(and(xa,xb),and(xa,xc)))))))). % INH4 prove ((({xa} ({xb} (~inh(xb) v inh(or(xa,xb))))) & ({xa} (~inh(xa) v inh(or(xa,xb)))) & ({xb} ({xa} (~inh(and(xa,xb)) v inh(xb)))) & ({xa} (~inh(and(xa,xb)) v inh(xa))) & ({xa} ({xb} (~inh(xa) v ~inh(xb) v inh(and(xa,xb)))))) => (({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) => ({xc} ({xb} ({xa} (inh(and(xa,or(xb,xc))) => inh(or(and(xa,xb),and(xa,xc))))))))). % INH4.1 prove ((({xa} ({xb} (~inh(xb) v inh(or(xa,xb))))) & ({xa} (~inh(xa) v inh(or(xa,xb)))) & ({xb} ({xa} (~inh(and(xa,xb)) v inh(xb)))) & ({xa} (~inh(and(xa,xb)) v inh(xa))) & ({xa} ({xb} (~inh(xa) v ~inh(xb) v inh(and(xa,xb))))) & inh(and(a,or(b,c)))) => (({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) => inh(or(and(a,b),and(a,c))))). % INH5 prove ((({xa} ({xb} (~inh(xb) v inh(or(xa,xb))))) & ({xa} (~inh(xa) v inh(or(xa,xb)))) & ({xa} ({xb} (~inh(xa) v ~inh(xb) v inh(and(xa,xb)))))) => (({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) => ({xc} ({xb} (inh(or(xb,xc)) => inh(or(and(xb,xb),xc))))))). % INH6 prove ((({xa} ({xb} (~inh(xb) v inh(or(xa,xb))))) & ({xa} (~inh(xa) v inh(or(xa,xb)))) & ({xa} ({xb} (~inh(xa) v ~inh(xb) v inh(and(xa,xb))))) & inh(or(b,c))) => (({xc} ({xb} ({xa} (((inh(xa) => inh(xc)) & (inh(xb) => inh(xc)) & inh(or(xa,xb))) => inh(xc))))) => inh(or(and(b,b),c)))). % SYNTH1 prove ((({x} eq(x,x)) & ({x} ~m(x,nil)) & ~eq(0,1) & ({x} ({y} (~eq(x,y) v m(x,c(y,z))))) & ({x} ({y} (~m(x,z) v m(x,c(y,z)))))) => ((({x} ({y} (m(x,y) v ~m(x,y)))) & ({x} ({y} ({z} (m(x,c(y,z)) => (eq(x,y) v m(x,z))))))) => ({x} ( ((m(0,x) => eq(y,1)) & (eq(y,1) => m(0,x))))))). % SYNTH1 prove ((({x} eq(x,x)) & ({x} ~m(x,nil)) & ~eq(0,1) & ({x} ({y} (~eq(x,y) v m(x,c(y,z))))) & ({x} ({y} (~m(x,z) v m(x,c(y,z)))))) => ((({x} ({y} (m(x,y) v ~m(x,y)))) & ({x} ({y} ({z} (m(x,c(y,z)) => (eq(x,y) v m(x,z))))))) => ({x} ( ((m(0,x) => eq(y,1)) & (eq(y,1) => m(0,x))))))). % SYNTHM prove ((({x} eq(x,x)) & ({x} ~m(x,nil)) & ~eq(0,1) & ({x} ({y} (eq(x,y) => m(x,c(y,z))))) & ({x} ({y} ({z} (m(x,z) => m(x,c(y,z)))))) & ({x} ({y} (eq(x,y) v ~eq(x,y)))) & ({x} ({y} ({z} (m(x,c(y,z)) => (eq(x,y) v m(x,z))))))) => ({x} (( ((m(0,x) => eq(y,1)) & (eq(y,1) => m(0,x)))) => ({v} ( ((m(0,c(v,x)) => eq(u,1)) & (eq(u,1) => m(0,c(v,x))))))))). % TEST prove ((eq(a,b) & ({x} eq(x,x)) & ({y} ({x} (~eq(x,y) v ~p(x) v p(y))))) => (p(a) => p(b))). % THIERRY1 prove ((({x} ({y} ~(l(x,y) & l(y,x)))) & ({x1} ({y1} ({z1} (l(x1,y1) => (l(x1,z1) v l(z1,y1))))))) => ({x2} ({y2} ({z2} (l(x2,y2) => (l(y2,z2) => l(x2,z2))))))). % LIFSCHITZ prove ~~( ( ({y} ( ( ((~p(y,y) v (p(x,x) v ~s(z,x))) & ((s(x,y) v (~s(y,z) v q(z1,z1))) & (q(x1,y) v (~q(y,z1) v s(x1,x1)))))))))). % LIFSCHITZ1 prove ~~( ( ({y} ( ( (~p(y,y) v (p(x,x) v ~s(z,x)))))))). % LIFSCHITZ2 prove ~~( ({y} ( ( (s(x,y) v (~s(y,z) v q(z1,z1))))))). % LIFSCHITZ2-1 prove ~~( ({y} ( (s(x,y) v ~s(y,z))))). % LIFSCHITZ2-3 prove ~~({y} ( (s(y) v ~s(z)))). % LIFSCHITZ2-4 prove ({y} ( (s(z) & ~s(y)))). % LIFSCHITZ3 prove ~~( ( ({y} ( ( (q(x1,y) v (~q(y,z1) v s(x1,x1)))))))). % EX prove (~(a(c) & b(c)) => (~a(c) v ~b(c))). % EX1 prove (~~a(c) => a(c)). % LO1 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} ~g(x,x))). % LO2 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} ({y} (g(x,y) => ~g(y,x))))). % LO3 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} ({y} ({z} ((g(x,y) & g(y,z)) => g(x,z)))))). % LO4 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} (~g(x,x) v g(x,x)))). % LO5 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} ({y} ({z} ((g(x,y) v g(y,x)) => ((g(x,z) v g(z,x)) v (g(y,z) v g(z,y)))))))). % LO6 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} ({y} (g(x,y) => ~g(y,x))))). % LO7 prove ((({x} ({y} ~(g(x,y) & g(y,x)))) & ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))) => ({x} ({y} ({z} ((g(x,y) & ~g(z,y)) => g(x,z)))))). % LOM1 prove ((({x} ({y} ({z} ((g(x,y) v g(y,x)) => ((g(x,z) v g(z,x)) v (g(y,z) v g(z,y))))))) & ({x} ({y} ({z} ((g(x,y) & g(y,z)) => g(x,z)))))) => ({x} ({y} ({z} (g(x,y) => (g(x,z) v g(z,y))))))). % VP2 prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} (dipt(x,y) => ~apt(x,ln(x,y))))) & ({x} ({y} (dipt(x,y) => ~apt(y,ln(x,y))))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),x)))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),y)))) & ({x} ({y} ({u} ({v} ((dipt(x,y) & diln(u,v)) => ((apt(x,u) v apt(x,v)) v (apt(y,u) v apt(y,v)))))))) & ({x} ({y} ({z} (apt(x,y) => (dipt(x,z) v apt(z,y)))))) & ({x} ({y} ({z} (apt(x,y) => (diln(y,z) v apt(x,z)))))) & ({x} ({y} ({z} (con(x,y) => (diln(y,z) v con(x,z))))))) => ({x} ({y} ({z} ((con(x,y) & ~apt(z,x) & ~apt(z,y)) => ~dipt(z,pt(x,y))))))). % VP2S prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} (dipt(x,y) => ~apt(x,ln(x,y))))) & ({x} ({y} (dipt(x,y) => ~apt(y,ln(x,y))))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),x)))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),y)))) & ({x} ({y} ({u} ({v} ((dipt(x,y) & diln(u,v)) => ((apt(x,u) v apt(x,v)) v (apt(y,u) v apt(y,v)))))))) & ({x} ({y} (con(x,y) => diln(x,y)))) & ({x} ({y} ({z} (apt(x,y) => (dipt(x,z) v apt(z,y)))))) & ({x} ({y} ({z} (apt(x,y) => (diln(y,z) v apt(x,z)))))) & ({x} ({y} ({z} (con(x,y) => (diln(y,z) v con(x,z))))))) => ({x} ({y} ({z} ((con(x,y) & ~apt(z,x) & ~apt(z,y)) => ~dipt(z,pt(x,y))))))). % VP2SS prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} (dipt(x,y) => ~apt(x,ln(x,y))))) & ({x} ({y} (dipt(x,y) => ~apt(y,ln(x,y))))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),x)))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),y)))) & ({x} ({y} ({u} ({v} ((dipt(x,y) & diln(u,v)) => ((apt(x,u) v apt(x,v)) v (apt(y,u) v apt(y,v)))))))) & ({x} ({y} (con(x,y) => diln(x,y))))) => ({x} ({y} ({z} ((con(x,y) & ~apt(z,x) & ~apt(z,y)) => ~dipt(z,pt(x,y))))))). % VP3 prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} (dipt(x,y) => ~apt(x,ln(x,y))))) & ({x} ({y} (dipt(x,y) => ~apt(y,ln(x,y))))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),x)))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),y)))) & ({x} ({y} ({u} ({v} ((dipt(x,y) & diln(u,v)) => ((apt(x,u) v apt(x,v)) v (apt(y,u) v apt(y,v)))))))) & ({x} ({y} ({z} (apt(x,y) => (dipt(x,z) v apt(z,y)))))) & ({x} ({y} ({z} (apt(x,y) => (diln(y,z) v apt(x,z)))))) & ({x} ({y} ({z} (con(x,y) => (diln(y,z) v con(x,z))))))) => ({x} ({y} (con(x,y) => diln(x,y))))). % VP3S prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} (dipt(x,y) => ~apt(x,ln(x,y))))) & ({x} ({y} (dipt(x,y) => ~apt(y,ln(x,y))))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),x)))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),y)))) & ({x} ({y} ({z} (apt(x,y) => (dipt(x,z) v apt(z,y)))))) & ({x} ({y} ({z} (apt(x,y) => (diln(y,z) v apt(x,z)))))) & ({x} ({y} ({z} (con(x,y) => (diln(y,z) v con(x,z))))))) => ({x} ({y} (con(x,y) => diln(x,y))))). % VP3SS prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} ({z} (apt(x,y) => (dipt(x,z) v apt(z,y)))))) & ({x} ({y} ({z} (apt(x,y) => (diln(y,z) v apt(x,z)))))) & ({x} ({y} ({z} (con(x,y) => (diln(y,z) v con(x,z))))))) => ({x} ({y} (con(x,y) => diln(x,y))))). % VP1 prove ((({x} ~dipt(x,x)) & ({x} ~diln(x,x)) & ({x} ~con(x,x)) & ({x} ({y} ({z} (dipt(x,y) => (dipt(x,z) v dipt(y,z)))))) & ({x} ({y} ({z} (diln(x,y) => (diln(x,z) v diln(y,z)))))) & ({x} ({y} ({z} (con(x,y) => (con(x,z) v con(y,z)))))) & ({x} ({y} (dipt(x,y) => ~apt(x,ln(x,y))))) & ({x} ({y} (dipt(x,y) => ~apt(y,ln(x,y))))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),x)))) & ({x} ({y} (con(x,y) => ~apt(pt(x,y),y)))) & ({x} ({y} ({u} ({v} ((dipt(x,y) & diln(u,v)) => ((apt(x,u) v apt(x,v)) v (apt(y,u) v apt(y,v))))))))) => ({x} ({y} ({u} ((dipt(x,y) & (~apt(x,u) & ~apt(y,u))) => ~diln(u,ln(x,y))))))). % BEZEM prove ((({x} (p(x) v ~p(x))) & ({y} (d(y) v ~d(y)))) => (~( ((p(x) & d(x)) => ({y} (p(y) => d(y))))) => ~( p(x)))).