%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM841+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:53:24 AM UTC 2026
% Result : Theorem 194.24s 194.56s
% Output : Proof 195.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM841+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 19:21:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 194.24/194.56 % SZS status Theorem for theBenchmark
% 194.24/194.56 % SZS output start Proof for theBenchmark
% 195.44/195.70 fof(holds(214, 352, 0), conjecture,
% 195.44/195.70 greater(vplus(vd344, vd347), vplus(vd345, vd348)),
% 195.44/195.70 file('theBenchmark.p', holds(214, 352, 0)) ).
% 195.44/195.70
% 195.44/195.70 fof(holds(213, 351, 2), axiom,
% 195.44/195.70 vplus(vd348, vd345) = vplus(vd345, vd348),
% 195.44/195.70 file('theBenchmark.p', holds(213, 351, 2)) ).
% 195.44/195.70
% 195.44/195.70 fof(holds(213, 351, 1), axiom,
% 195.44/195.70 greater(vplus(vd347, vd345), vplus(vd348, vd345)),
% 195.44/195.70 file('theBenchmark.p', holds(213, 351, 1)) ).
% 195.44/195.70
% 195.44/195.70 fof(holds(213, 351, 0), axiom,
% 195.44/195.70 vplus(vd345, vd347) = vplus(vd347, vd345),
% 195.44/195.70 file('theBenchmark.p', holds(213, 351, 0)) ).
% 195.44/195.70
% 195.44/195.70 fof(holds(212, 350, 0), axiom,
% 195.44/195.70 greater(vplus(vd344, vd347), vplus(vd345, vd347)),
% 195.44/195.70 file('theBenchmark.p', holds(212, 350, 0)) ).
% 195.44/195.70
% 195.44/195.70 fof(holds(conjunct2(211), 349, 0), axiom,
% 195.44/195.70 greater(vd347, vd348),
% 195.44/195.70 file('theBenchmark.p', holds(conjunct2(211), 349, 0)) ).
% 195.44/195.70
% 195.44/195.70 fof(holds(conjunct1(211), 346, 0), axiom,
% 195.44/195.70 greater(vd344, vd345),
% 195.44/195.70 file('theBenchmark.p', holds(conjunct1(211), 346, 0)) ).
% 195.44/195.70
% 195.44/195.70 fof(ass(cond(goal(202), 0), 0), axiom,
% 195.44/195.70 ! [ Vd328,Vd329,Vd330 ] : ( less(vplus(Vd328, Vd330), vplus(Vd329, Vd330)) => less(Vd328, Vd329) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(202), 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(202), 0), 1), axiom,
% 195.44/195.71 ! [ Vd328,Vd329,Vd330 ] : ( vplus(Vd328, Vd330) = vplus(Vd329, Vd330) => Vd328 = Vd329 ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(202), 0), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(202), 0), 2), axiom,
% 195.44/195.71 ! [ Vd328,Vd329,Vd330 ] : ( greater(vplus(Vd328, Vd330), vplus(Vd329, Vd330)) => greater(Vd328, Vd329) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(202), 0), 2)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(193), 0), 0), axiom,
% 195.44/195.71 ! [ Vd301,Vd302,Vd303 ] : ( less(Vd301, Vd302) => less(vplus(Vd301, Vd303), vplus(Vd302, Vd303)) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(193), 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(193), 0), 1), axiom,
% 195.44/195.71 ! [ Vd301,Vd302,Vd303 ] : ( Vd301 = Vd302 => vplus(Vd301, Vd303) = vplus(Vd302, Vd303) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(193), 0), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(193), 0), 2), axiom,
% 195.44/195.71 ! [ Vd301,Vd302,Vd303 ] : ( greater(Vd301, Vd302) => greater(vplus(Vd301, Vd303), vplus(Vd302, Vd303)) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(193), 0), 2)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(189, 0), 0), axiom,
% 195.44/195.71 ! [ Vd295,Vd296 ] : greater(vplus(Vd295, Vd296), Vd295),
% 195.44/195.71 file('theBenchmark.p', ass(cond(189, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(184, 0), 0), axiom,
% 195.44/195.71 ! [ Vd289,Vd290,Vd292 ] : ( ( leq(Vd290, Vd292) & leq(Vd289, Vd290) ) => leq(Vd289, Vd292) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(184, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(177), 0), 0), axiom,
% 195.44/195.71 ! [ Vd281,Vd282,Vd283 ] : ( ( ( less(Vd282, Vd283) & leq(Vd281, Vd282) ) | ( leq(Vd282, Vd283) & less(Vd281, Vd282) ) ) => less(Vd281, Vd283) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(177), 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(168, 0), 0), axiom,
% 195.44/195.71 ! [ Vd262,Vd263,Vd265 ] : ( ( less(Vd263, Vd265) & less(Vd262, Vd263) ) => less(Vd262, Vd265) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(168, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(163, 0), 0), axiom,
% 195.44/195.71 ! [ Vd258,Vd259 ] : ( leq(Vd258, Vd259) => geq(Vd259, Vd258) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(163, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(158, 0), 0), axiom,
% 195.44/195.71 ! [ Vd254,Vd255 ] : ( geq(Vd254, Vd255) => leq(Vd255, Vd254) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(158, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(def(cond(conseq(axiom(3)), 17), 1), axiom,
% 195.44/195.71 ! [ Vd249,Vd250 ] : ( leq(Vd250, Vd249) <=> ( less(Vd250, Vd249) | Vd250 = Vd249 ) ),
% 195.44/195.71 file('theBenchmark.p', def(cond(conseq(axiom(3)), 17), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(def(cond(conseq(axiom(3)), 16), 1), axiom,
% 195.44/195.71 ! [ Vd244,Vd245 ] : ( geq(Vd245, Vd244) <=> ( greater(Vd245, Vd244) | Vd245 = Vd244 ) ),
% 195.44/195.71 file('theBenchmark.p', def(cond(conseq(axiom(3)), 16), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(147, 0), 0), axiom,
% 195.44/195.71 ! [ Vd226,Vd227 ] : ( less(Vd226, Vd227) => greater(Vd227, Vd226) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(147, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(140, 0), 0), axiom,
% 195.44/195.71 ! [ Vd208,Vd209 ] : ( greater(Vd208, Vd209) => less(Vd209, Vd208) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(140, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(130), 0), 0), axiom,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( Vd203 = Vd204 | greater(Vd203, Vd204) | less(Vd203, Vd204) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(130), 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(130), 0), 1), axiom,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( ~( Vd203 = Vd204 ) | ~( less(Vd203, Vd204) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(130), 0), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(130), 0), 2), axiom,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( ~( greater(Vd203, Vd204) ) | ~( less(Vd203, Vd204) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(130), 0), 2)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(130), 0), 3), axiom,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( ~( Vd203 = Vd204 ) | ~( greater(Vd203, Vd204) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(130), 0), 3)) ).
% 195.44/195.71
% 195.44/195.71 fof(def(cond(conseq(axiom(3)), 12), 1), axiom,
% 195.44/195.71 ! [ Vd198,Vd199 ] : ( less(Vd199, Vd198) <=> ? [ Vd201 ] : Vd198 = vplus(Vd199, Vd201) ),
% 195.44/195.71 file('theBenchmark.p', def(cond(conseq(axiom(3)), 12), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(def(cond(conseq(axiom(3)), 11), 1), axiom,
% 195.44/195.71 ! [ Vd193,Vd194 ] : ( greater(Vd194, Vd193) <=> ? [ Vd196 ] : Vd194 = vplus(Vd193, Vd196) ),
% 195.44/195.71 file('theBenchmark.p', def(cond(conseq(axiom(3)), 11), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(88), 0), 0), axiom,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( Vd120 = Vd121 | ? [ Vd123 ] : Vd120 = vplus(Vd121, Vd123) | ? [ Vd125 ] : Vd121 = vplus(Vd120, Vd125) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(88), 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(88), 0), 1), axiom,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( ~( Vd120 = Vd121 ) | ~( ? [ Vd125 ] : Vd121 = vplus(Vd120, Vd125) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(88), 0), 1)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(88), 0), 2), axiom,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( ~( ? [ Vd123 ] : Vd120 = vplus(Vd121, Vd123) ) | ~( ? [ Vd125 ] : Vd121 = vplus(Vd120, Vd125) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(88), 0), 2)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(goal(88), 0), 3), axiom,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( ~( Vd120 = Vd121 ) | ~( ? [ Vd123 ] : Vd120 = vplus(Vd121, Vd123) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(goal(88), 0), 3)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(81, 0), 0), axiom,
% 195.44/195.71 ! [ Vd104,Vd105 ] : ( ~( Vd104 = Vd105 ) => ! [ Vd107 ] : ~( vplus(Vd107, Vd104) = vplus(Vd107, Vd105) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(81, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(73, 0), 0), axiom,
% 195.44/195.71 ! [ Vd92,Vd93 ] : ~( Vd93 = vplus(Vd92, Vd93) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(73, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(61, 0), 0), axiom,
% 195.44/195.71 ! [ Vd78,Vd79 ] : vplus(Vd79, Vd78) = vplus(Vd78, Vd79),
% 195.44/195.71 file('theBenchmark.p', ass(cond(61, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(52, 0), 0), axiom,
% 195.44/195.71 ! [ Vd68,Vd69 ] : vplus(vsucc(Vd68), Vd69) = vsucc(vplus(Vd68, Vd69)),
% 195.44/195.71 file('theBenchmark.p', ass(cond(52, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(43, 0), 0), axiom,
% 195.44/195.71 ! [ Vd59 ] : vplus(v1, Vd59) = vsucc(Vd59),
% 195.44/195.71 file('theBenchmark.p', ass(cond(43, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(33, 0), 0), axiom,
% 195.44/195.71 ! [ Vd46,Vd47,Vd48 ] : vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)),
% 195.44/195.71 file('theBenchmark.p', ass(cond(33, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0))), axiom,
% 195.44/195.71 ! [ Vd42,Vd43 ] : ( vplus(Vd42, vsucc(Vd43)) = vsucc(vplus(Vd42, Vd43)) & vplus(Vd42, v1) = vsucc(Vd42) ),
% 195.44/195.71 file('theBenchmark.p', qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(20, 0), 0), axiom,
% 195.44/195.71 ! [ Vd24 ] : ( ~( Vd24 = v1 ) => Vd24 = vsucc(vskolem2(Vd24)) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(20, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(12, 0), 0), axiom,
% 195.44/195.71 ! [ Vd16 ] : ~( vsucc(Vd16) = Vd16 ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(12, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(ass(cond(6, 0), 0), axiom,
% 195.44/195.71 ! [ Vd7,Vd8 ] : ( ~( Vd7 = Vd8 ) => ~( vsucc(Vd7) = vsucc(Vd8) ) ),
% 195.44/195.71 file('theBenchmark.p', ass(cond(6, 0), 0)) ).
% 195.44/195.71
% 195.44/195.71 fof(qu(antec(axiom(3)), imp(antec(axiom(3)))), axiom,
% 195.44/195.71 ! [ Vd3,Vd4 ] : ( vsucc(Vd3) = vsucc(Vd4) => Vd3 = Vd4 ),
% 195.44/195.71 file('theBenchmark.p', qu(antec(axiom(3)), imp(antec(axiom(3))))) ).
% 195.44/195.71
% 195.44/195.71 fof(qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0)), axiom,
% 195.44/195.71 ! [ Vd1 ] : ~( vsucc(Vd1) = v1 ),
% 195.44/195.71 file('theBenchmark.p', qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))) ).
% 195.44/195.71
% 195.44/195.71 fof(f_1_1, negated_conjecture,
% 195.44/195.71 ~( greater(vplus(vd344, vd347), vplus(vd345, vd348)) ),
% 195.44/195.71 inference(negate,[status(cth)],[holds(214, 352, 0)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_1_2, negated_conjecture,
% 195.44/195.71 ( ~greater(vplus(vd344, vd347), vplus(vd345, vd348)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_1_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_2_1, plain,
% 195.44/195.71 vplus(vd348, vd345) = vplus(vd345, vd348),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[holds(213, 351, 2)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_2_2, plain,
% 195.44/195.71 ( vplus(vd348, vd345) = vplus(vd345, vd348) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_2_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_3_1, plain,
% 195.44/195.71 greater(vplus(vd347, vd345), vplus(vd348, vd345)),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[holds(213, 351, 1)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_3_2, plain,
% 195.44/195.71 ( greater(vplus(vd347, vd345), vplus(vd348, vd345)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_3_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_4_1, plain,
% 195.44/195.71 vplus(vd345, vd347) = vplus(vd347, vd345),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[holds(213, 351, 0)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_4_2, plain,
% 195.44/195.71 ( vplus(vd345, vd347) = vplus(vd347, vd345) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_4_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_5_1, plain,
% 195.44/195.71 greater(vplus(vd344, vd347), vplus(vd345, vd347)),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[holds(212, 350, 0)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_5_2, plain,
% 195.44/195.71 ( greater(vplus(vd344, vd347), vplus(vd345, vd347)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_5_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_6_1, plain,
% 195.44/195.71 greater(vd347, vd348),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[holds(conjunct2(211), 349, 0)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_6_2, plain,
% 195.44/195.71 ( greater(vd347, vd348) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_6_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_7_1, plain,
% 195.44/195.71 greater(vd344, vd345),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[holds(conjunct1(211), 346, 0)]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_7_2, plain,
% 195.44/195.71 ( greater(vd344, vd345) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_7_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_8_1, plain,
% 195.44/195.71 ! [ Vd328,Vd329,Vd330 ] : ( ~( less(vplus(Vd328, Vd330), vplus(Vd329, Vd330)) ) | less(Vd328, Vd329) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(202), 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_8_2, plain,
% 195.44/195.71 ! [ U_2,U_1,U_0 ] : ( ~( less(vplus(U_2, U_0), vplus(U_1, U_0)) ) | less(U_2, U_1) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_8_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_8_3, plain,
% 195.44/195.71 ! [ U_2,U_1 ] : ( less(U_2, U_1) | ! [ U_0 ] : ~( less(vplus(U_2, U_0), vplus(U_1, U_0)) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_8_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_8_4, plain,
% 195.44/195.71 ( less(U_2, U_1) | ~less(vplus(U_2, U_0), vplus(U_1, U_0)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_8_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_9_1, plain,
% 195.44/195.71 ! [ Vd328,Vd329,Vd330 ] : ( ~( vplus(Vd328, Vd330) = vplus(Vd329, Vd330) ) | Vd328 = Vd329 ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(202), 0), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_9_2, plain,
% 195.44/195.71 ! [ U_5,U_4,U_3 ] : ( ~( vplus(U_5, U_3) = vplus(U_4, U_3) ) | U_5 = U_4 ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_9_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_9_3, plain,
% 195.44/195.71 ! [ U_5,U_4 ] : ( U_5 = U_4 | ! [ U_3 ] : ~( vplus(U_5, U_3) = vplus(U_4, U_3) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_9_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_9_4, plain,
% 195.44/195.71 ( U_5 = U_4 | vplus(U_5, U_3) != vplus(U_4, U_3) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_9_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_10_1, plain,
% 195.44/195.71 ! [ Vd328,Vd329,Vd330 ] : ( ~( greater(vplus(Vd328, Vd330), vplus(Vd329, Vd330)) ) | greater(Vd328, Vd329) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(202), 0), 2)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_10_2, plain,
% 195.44/195.71 ! [ U_8,U_7,U_6 ] : ( ~( greater(vplus(U_8, U_6), vplus(U_7, U_6)) ) | greater(U_8, U_7) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_10_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_10_3, plain,
% 195.44/195.71 ! [ U_8,U_7 ] : ( greater(U_8, U_7) | ! [ U_6 ] : ~( greater(vplus(U_8, U_6), vplus(U_7, U_6)) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_10_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_10_4, plain,
% 195.44/195.71 ( greater(U_8, U_7) | ~greater(vplus(U_8, U_6), vplus(U_7, U_6)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_10_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_11_1, plain,
% 195.44/195.71 ! [ Vd301,Vd302,Vd303 ] : ( ~( less(Vd301, Vd302) ) | less(vplus(Vd301, Vd303), vplus(Vd302, Vd303)) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(193), 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_11_2, plain,
% 195.44/195.71 ! [ U_11,U_10,U_9 ] : ( ~( less(U_11, U_10) ) | less(vplus(U_11, U_9), vplus(U_10, U_9)) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_11_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_11_3, plain,
% 195.44/195.71 ! [ U_11,U_10 ] : ( ~( less(U_11, U_10) ) | ! [ U_9 ] : less(vplus(U_11, U_9), vplus(U_10, U_9)) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_11_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_11_4, plain,
% 195.44/195.71 ( ~less(U_11, U_10) | less(vplus(U_11, U_9), vplus(U_10, U_9)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_11_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_12_1, plain,
% 195.44/195.71 ! [ Vd301,Vd302,Vd303 ] : ( ~( Vd301 = Vd302 ) | vplus(Vd301, Vd303) = vplus(Vd302, Vd303) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(193), 0), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_12_2, plain,
% 195.44/195.71 ! [ U_14,U_13,U_12 ] : ( ~( U_14 = U_13 ) | vplus(U_14, U_12) = vplus(U_13, U_12) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_12_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_12_3, plain,
% 195.44/195.71 ! [ U_14,U_13 ] : ( ~( U_14 = U_13 ) | ! [ U_12 ] : vplus(U_14, U_12) = vplus(U_13, U_12) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_12_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_12_4, plain,
% 195.44/195.71 ( U_14 != U_13 | vplus(U_14, U_12) = vplus(U_13, U_12) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_12_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_13_1, plain,
% 195.44/195.71 ! [ Vd301,Vd302,Vd303 ] : ( ~( greater(Vd301, Vd302) ) | greater(vplus(Vd301, Vd303), vplus(Vd302, Vd303)) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(193), 0), 2)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_13_2, plain,
% 195.44/195.71 ! [ U_17,U_16,U_15 ] : ( ~( greater(U_17, U_16) ) | greater(vplus(U_17, U_15), vplus(U_16, U_15)) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_13_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_13_3, plain,
% 195.44/195.71 ! [ U_17,U_16 ] : ( ~( greater(U_17, U_16) ) | ! [ U_15 ] : greater(vplus(U_17, U_15), vplus(U_16, U_15)) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_13_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_13_4, plain,
% 195.44/195.71 ( ~greater(U_17, U_16) | greater(vplus(U_17, U_15), vplus(U_16, U_15)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_13_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_14_1, plain,
% 195.44/195.71 ! [ Vd295,Vd296 ] : greater(vplus(Vd295, Vd296), Vd295),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(189, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_14_2, plain,
% 195.44/195.71 ! [ U_19,U_18 ] : greater(vplus(U_19, U_18), U_19),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_14_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_14_3, plain,
% 195.44/195.71 ( greater(vplus(U_19, U_18), U_19) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_14_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_15_1, plain,
% 195.44/195.71 ! [ Vd289,Vd290,Vd292 ] : ( ( ~( leq(Vd290, Vd292) ) | ~( leq(Vd289, Vd290) ) ) | leq(Vd289, Vd292) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(184, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_15_2, plain,
% 195.44/195.71 ! [ U_22,U_21,U_20 ] : ( ( ~( leq(U_21, U_20) ) | ~( leq(U_22, U_21) ) ) | leq(U_22, U_20) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_15_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_15_3, plain,
% 195.44/195.71 ( ~leq(U_21, U_20) | ~leq(U_22, U_21) | leq(U_22, U_20) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_15_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_16_1, plain,
% 195.44/195.71 ! [ Vd281,Vd282,Vd283 ] : ( ( ( ~( less(Vd282, Vd283) ) | ~( leq(Vd281, Vd282) ) ) & ( ~( leq(Vd282, Vd283) ) | ~( less(Vd281, Vd282) ) ) ) | less(Vd281, Vd283) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(177), 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_16_2, plain,
% 195.44/195.71 ! [ U_25,U_24,U_23 ] : ( ( ( ~( less(U_24, U_23) ) | ~( leq(U_25, U_24) ) ) & ( ~( leq(U_24, U_23) ) | ~( less(U_25, U_24) ) ) ) | less(U_25, U_23) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_16_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_16_3, plain,
% 195.44/195.71 ( less(U_25, U_23) | ~less(U_24, U_23) | ~leq(U_25, U_24) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_16_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_16_4, plain,
% 195.44/195.71 ( less(U_25, U_23) | ~leq(U_24, U_23) | ~less(U_25, U_24) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_16_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_17_1, plain,
% 195.44/195.71 ! [ Vd262,Vd263,Vd265 ] : ( ( ~( less(Vd263, Vd265) ) | ~( less(Vd262, Vd263) ) ) | less(Vd262, Vd265) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(168, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_17_2, plain,
% 195.44/195.71 ! [ U_28,U_27,U_26 ] : ( ( ~( less(U_27, U_26) ) | ~( less(U_28, U_27) ) ) | less(U_28, U_26) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_17_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_17_3, plain,
% 195.44/195.71 ( ~less(U_27, U_26) | ~less(U_28, U_27) | less(U_28, U_26) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_17_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_18_1, plain,
% 195.44/195.71 ! [ Vd258,Vd259 ] : ( ~( leq(Vd258, Vd259) ) | geq(Vd259, Vd258) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(163, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_18_2, plain,
% 195.44/195.71 ! [ U_30,U_29 ] : ( ~( leq(U_30, U_29) ) | geq(U_29, U_30) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_18_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_18_3, plain,
% 195.44/195.71 ( ~leq(U_30, U_29) | geq(U_29, U_30) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_18_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_19_1, plain,
% 195.44/195.71 ! [ Vd254,Vd255 ] : ( ~( geq(Vd254, Vd255) ) | leq(Vd255, Vd254) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(158, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_19_2, plain,
% 195.44/195.71 ! [ U_32,U_31 ] : ( ~( geq(U_32, U_31) ) | leq(U_31, U_32) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_19_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_19_3, plain,
% 195.44/195.71 ( ~geq(U_32, U_31) | leq(U_31, U_32) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_19_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_20_1, plain,
% 195.44/195.71 ! [ Vd249,Vd250 ] : ( ( ~( leq(Vd250, Vd249) ) | ( less(Vd250, Vd249) | Vd250 = Vd249 ) ) & ( ( ~( less(Vd250, Vd249) ) & ~( Vd250 = Vd249 ) ) | leq(Vd250, Vd249) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[def(cond(conseq(axiom(3)), 17), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_20_2, plain,
% 195.44/195.71 ! [ U_34,U_33 ] : ( ( ~( leq(U_33, U_34) ) | ( less(U_33, U_34) | U_33 = U_34 ) ) & ( ( ~( less(U_33, U_34) ) & ~( U_33 = U_34 ) ) | leq(U_33, U_34) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_20_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_20_3, plain,
% 195.44/195.71 ( ! [ U_37,U_35 ] : ( ~( leq(U_35, U_37) ) | ( less(U_35, U_37) | U_35 = U_37 ) ) & ! [ U_38,U_36 ] : ( ( ~( less(U_36, U_38) ) & ~( U_36 = U_38 ) ) | leq(U_36, U_38) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_20_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_20_4, plain,
% 195.44/195.71 ( ~leq(U_35, U_37) | less(U_35, U_37) | U_35 = U_37 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_20_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_20_5, plain,
% 195.44/195.71 ( leq(U_36, U_38) | ~less(U_36, U_38) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_20_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_20_6, plain,
% 195.44/195.71 ( leq(U_36, U_38) | U_36 != U_38 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_20_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_21_1, plain,
% 195.44/195.71 ! [ Vd244,Vd245 ] : ( ( ~( geq(Vd245, Vd244) ) | ( greater(Vd245, Vd244) | Vd245 = Vd244 ) ) & ( ( ~( greater(Vd245, Vd244) ) & ~( Vd245 = Vd244 ) ) | geq(Vd245, Vd244) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[def(cond(conseq(axiom(3)), 16), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_21_2, plain,
% 195.44/195.71 ! [ U_40,U_39 ] : ( ( ~( geq(U_39, U_40) ) | ( greater(U_39, U_40) | U_39 = U_40 ) ) & ( ( ~( greater(U_39, U_40) ) & ~( U_39 = U_40 ) ) | geq(U_39, U_40) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_21_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_21_3, plain,
% 195.44/195.71 ( ! [ U_43,U_41 ] : ( ~( geq(U_41, U_43) ) | ( greater(U_41, U_43) | U_41 = U_43 ) ) & ! [ U_44,U_42 ] : ( ( ~( greater(U_42, U_44) ) & ~( U_42 = U_44 ) ) | geq(U_42, U_44) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_21_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_21_4, plain,
% 195.44/195.71 ( ~geq(U_41, U_43) | greater(U_41, U_43) | U_41 = U_43 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_21_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_21_5, plain,
% 195.44/195.71 ( geq(U_42, U_44) | ~greater(U_42, U_44) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_21_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_21_6, plain,
% 195.44/195.71 ( geq(U_42, U_44) | U_42 != U_44 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_21_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_22_1, plain,
% 195.44/195.71 ! [ Vd226,Vd227 ] : ( ~( less(Vd226, Vd227) ) | greater(Vd227, Vd226) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(147, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_22_2, plain,
% 195.44/195.71 ! [ U_46,U_45 ] : ( ~( less(U_46, U_45) ) | greater(U_45, U_46) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_22_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_22_3, plain,
% 195.44/195.71 ( ~less(U_46, U_45) | greater(U_45, U_46) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_22_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_23_1, plain,
% 195.44/195.71 ! [ Vd208,Vd209 ] : ( ~( greater(Vd208, Vd209) ) | less(Vd209, Vd208) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(140, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_23_2, plain,
% 195.44/195.71 ! [ U_48,U_47 ] : ( ~( greater(U_48, U_47) ) | less(U_47, U_48) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_23_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_23_3, plain,
% 195.44/195.71 ( ~greater(U_48, U_47) | less(U_47, U_48) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_23_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_24_1, plain,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( Vd203 = Vd204 | greater(Vd203, Vd204) | less(Vd203, Vd204) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(130), 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_24_2, plain,
% 195.44/195.71 ! [ U_50,U_49 ] : ( U_50 = U_49 | greater(U_50, U_49) | less(U_50, U_49) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_24_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_24_3, plain,
% 195.44/195.71 ( U_50 = U_49 | greater(U_50, U_49) | less(U_50, U_49) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_24_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_25_1, plain,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( ~( Vd203 = Vd204 ) | ~( less(Vd203, Vd204) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(130), 0), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_25_2, plain,
% 195.44/195.71 ! [ U_52,U_51 ] : ( ~( U_52 = U_51 ) | ~( less(U_52, U_51) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_25_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_25_3, plain,
% 195.44/195.71 ( U_52 != U_51 | ~less(U_52, U_51) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_25_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_26_1, plain,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( ~( greater(Vd203, Vd204) ) | ~( less(Vd203, Vd204) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(130), 0), 2)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_26_2, plain,
% 195.44/195.71 ! [ U_54,U_53 ] : ( ~( greater(U_54, U_53) ) | ~( less(U_54, U_53) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_26_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_26_3, plain,
% 195.44/195.71 ( ~greater(U_54, U_53) | ~less(U_54, U_53) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_26_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_27_1, plain,
% 195.44/195.71 ! [ Vd203,Vd204 ] : ( ~( Vd203 = Vd204 ) | ~( greater(Vd203, Vd204) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(130), 0), 3)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_27_2, plain,
% 195.44/195.71 ! [ U_56,U_55 ] : ( ~( U_56 = U_55 ) | ~( greater(U_56, U_55) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_27_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_27_3, plain,
% 195.44/195.71 ( U_56 != U_55 | ~greater(U_56, U_55) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_27_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_28_1, plain,
% 195.44/195.71 ! [ Vd198,Vd199 ] : ( ( ~( less(Vd199, Vd198) ) | ? [ Vd201 ] : Vd198 = vplus(Vd199, Vd201) ) & ( ! [ Vd201 ] : ~( Vd198 = vplus(Vd199, Vd201) ) | less(Vd199, Vd198) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[def(cond(conseq(axiom(3)), 12), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_28_2, plain,
% 195.44/195.71 ! [ U_60,U_59 ] : ( ( ~( less(U_59, U_60) ) | ? [ U_57 ] : U_60 = vplus(U_59, U_57) ) & ( ! [ U_58 ] : ~( U_60 = vplus(U_59, U_58) ) | less(U_59, U_60) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_28_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_28_3, plain,
% 195.44/195.71 ( ! [ U_63,U_61 ] : ( ~( less(U_61, U_63) ) | ? [ U_57 ] : U_63 = vplus(U_61, U_57) ) & ! [ U_64,U_62 ] : ( ! [ U_58 ] : ~( U_64 = vplus(U_62, U_58) ) | less(U_62, U_64) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_28_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_28_4, plain,
% 195.44/195.71 ( ! [ U_63,U_61 ] : ( ~( less(U_61, U_63) ) | U_63 = vplus(U_61, sK1(U_63, U_61)) ) & ! [ U_64,U_62 ] : ( ! [ U_58 ] : ~( U_64 = vplus(U_62, U_58) ) | less(U_62, U_64) ) ),
% 195.44/195.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_57,sK1(U_63, U_61))],[f_28_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_28_5, plain,
% 195.44/195.71 ( ~less(U_61, U_63) | U_63 = vplus(U_61, sK1(U_63, U_61)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_28_4]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_28_6, plain,
% 195.44/195.71 ( U_64 != vplus(U_62, U_58) | less(U_62, U_64) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_28_4]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_29_1, plain,
% 195.44/195.71 ! [ Vd193,Vd194 ] : ( ( ~( greater(Vd194, Vd193) ) | ? [ Vd196 ] : Vd194 = vplus(Vd193, Vd196) ) & ( ! [ Vd196 ] : ~( Vd194 = vplus(Vd193, Vd196) ) | greater(Vd194, Vd193) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[def(cond(conseq(axiom(3)), 11), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_29_2, plain,
% 195.44/195.71 ! [ U_68,U_67 ] : ( ( ~( greater(U_67, U_68) ) | ? [ U_65 ] : U_67 = vplus(U_68, U_65) ) & ( ! [ U_66 ] : ~( U_67 = vplus(U_68, U_66) ) | greater(U_67, U_68) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_29_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_29_3, plain,
% 195.44/195.71 ( ! [ U_71,U_69 ] : ( ~( greater(U_69, U_71) ) | ? [ U_65 ] : U_69 = vplus(U_71, U_65) ) & ! [ U_72,U_70 ] : ( ! [ U_66 ] : ~( U_70 = vplus(U_72, U_66) ) | greater(U_70, U_72) ) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_29_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_29_4, plain,
% 195.44/195.71 ( ! [ U_71,U_69 ] : ( ~( greater(U_69, U_71) ) | U_69 = vplus(U_71, sK2(U_71, U_69)) ) & ! [ U_72,U_70 ] : ( ! [ U_66 ] : ~( U_70 = vplus(U_72, U_66) ) | greater(U_70, U_72) ) ),
% 195.44/195.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_65,sK2(U_71, U_69))],[f_29_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_29_5, plain,
% 195.44/195.71 ( ~greater(U_69, U_71) | U_69 = vplus(U_71, sK2(U_71, U_69)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_29_4]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_29_6, plain,
% 195.44/195.71 ( U_70 != vplus(U_72, U_66) | greater(U_70, U_72) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_29_4]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_30_1, plain,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( Vd120 = Vd121 | ? [ Vd123 ] : Vd120 = vplus(Vd121, Vd123) | ? [ Vd125 ] : Vd121 = vplus(Vd120, Vd125) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(88), 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_30_2, plain,
% 195.44/195.71 ! [ U_76,U_75 ] : ( U_76 = U_75 | ? [ U_73 ] : U_76 = vplus(U_75, U_73) | ? [ U_74 ] : U_75 = vplus(U_76, U_74) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_30_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_30_3, plain,
% 195.44/195.71 ! [ U_76,U_75 ] : ( U_76 = U_75 | U_76 = vplus(U_75, sK3(U_76, U_75)) | ? [ U_74 ] : U_75 = vplus(U_76, U_74) ),
% 195.44/195.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_73,sK3(U_76, U_75))],[f_30_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_30_4, plain,
% 195.44/195.71 ! [ U_76,U_75 ] : ( U_76 = U_75 | U_76 = vplus(U_75, sK3(U_76, U_75)) | U_75 = vplus(U_76, sK4(U_76, U_75)) ),
% 195.44/195.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_74,sK4(U_76, U_75))],[f_30_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_30_5, plain,
% 195.44/195.71 ( U_76 = U_75 | U_76 = vplus(U_75, sK3(U_76, U_75)) | U_75 = vplus(U_76, sK4(U_76, U_75)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_30_4]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_31_1, plain,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( ~( Vd120 = Vd121 ) | ! [ Vd125 ] : ~( Vd121 = vplus(Vd120, Vd125) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(88), 0), 1)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_31_2, plain,
% 195.44/195.71 ! [ U_79,U_78 ] : ( ~( U_79 = U_78 ) | ! [ U_77 ] : ~( U_78 = vplus(U_79, U_77) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_31_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_31_3, plain,
% 195.44/195.71 ( U_79 != U_78 | U_78 != vplus(U_79, U_77) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_31_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_32_1, plain,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( ! [ Vd123 ] : ~( Vd120 = vplus(Vd121, Vd123) ) | ! [ Vd125 ] : ~( Vd121 = vplus(Vd120, Vd125) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(88), 0), 2)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_32_2, plain,
% 195.44/195.71 ! [ U_83,U_82 ] : ( ! [ U_80 ] : ~( U_83 = vplus(U_82, U_80) ) | ! [ U_81 ] : ~( U_82 = vplus(U_83, U_81) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_32_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_32_3, plain,
% 195.44/195.71 ( U_83 != vplus(U_82, U_80) | U_82 != vplus(U_83, U_81) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_32_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_33_1, plain,
% 195.44/195.71 ! [ Vd120,Vd121 ] : ( ~( Vd120 = Vd121 ) | ! [ Vd123 ] : ~( Vd120 = vplus(Vd121, Vd123) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(goal(88), 0), 3)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_33_2, plain,
% 195.44/195.71 ! [ U_86,U_85 ] : ( ~( U_86 = U_85 ) | ! [ U_84 ] : ~( U_86 = vplus(U_85, U_84) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_33_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_33_3, plain,
% 195.44/195.71 ( U_86 != U_85 | U_86 != vplus(U_85, U_84) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_33_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_34_1, plain,
% 195.44/195.71 ! [ Vd104,Vd105 ] : ( Vd104 = Vd105 | ! [ Vd107 ] : ~( vplus(Vd107, Vd104) = vplus(Vd107, Vd105) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(81, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_34_2, plain,
% 195.44/195.71 ! [ U_89,U_88 ] : ( U_89 = U_88 | ! [ U_87 ] : ~( vplus(U_87, U_89) = vplus(U_87, U_88) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_34_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_34_3, plain,
% 195.44/195.71 ( U_89 = U_88 | vplus(U_87, U_89) != vplus(U_87, U_88) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_34_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_35_1, plain,
% 195.44/195.71 ! [ Vd92,Vd93 ] : ~( Vd93 = vplus(Vd92, Vd93) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(73, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_35_2, plain,
% 195.44/195.71 ! [ U_91,U_90 ] : ~( U_90 = vplus(U_91, U_90) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_35_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_35_3, plain,
% 195.44/195.71 ( U_90 != vplus(U_91, U_90) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_35_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_36_1, plain,
% 195.44/195.71 ! [ Vd78,Vd79 ] : vplus(Vd79, Vd78) = vplus(Vd78, Vd79),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(61, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_36_2, plain,
% 195.44/195.71 ! [ U_93,U_92 ] : vplus(U_92, U_93) = vplus(U_93, U_92),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_36_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_36_3, plain,
% 195.44/195.71 ( vplus(U_92, U_93) = vplus(U_93, U_92) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_36_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_37_1, plain,
% 195.44/195.71 ! [ Vd68,Vd69 ] : vplus(vsucc(Vd68), Vd69) = vsucc(vplus(Vd68, Vd69)),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(52, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_37_2, plain,
% 195.44/195.71 ! [ U_95,U_94 ] : vplus(vsucc(U_95), U_94) = vsucc(vplus(U_95, U_94)),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_37_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_37_3, plain,
% 195.44/195.71 ( vplus(vsucc(U_95), U_94) = vsucc(vplus(U_95, U_94)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_37_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_38_1, plain,
% 195.44/195.71 ! [ Vd59 ] : vplus(v1, Vd59) = vsucc(Vd59),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(43, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_38_2, plain,
% 195.44/195.71 ! [ U_96 ] : vplus(v1, U_96) = vsucc(U_96),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_38_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_38_3, plain,
% 195.44/195.71 ( vplus(v1, U_96) = vsucc(U_96) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_38_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_39_1, plain,
% 195.44/195.71 ! [ Vd46,Vd47,Vd48 ] : vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(33, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_39_2, plain,
% 195.44/195.71 ! [ U_99,U_98,U_97 ] : vplus(vplus(U_99, U_98), U_97) = vplus(U_99, vplus(U_98, U_97)),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_39_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_39_3, plain,
% 195.44/195.71 ( vplus(vplus(U_99, U_98), U_97) = vplus(U_99, vplus(U_98, U_97)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_39_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_40_1, plain,
% 195.44/195.71 ! [ Vd42,Vd43 ] : ( vplus(Vd42, vsucc(Vd43)) = vsucc(vplus(Vd42, Vd43)) & vplus(Vd42, v1) = vsucc(Vd42) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_40_2, plain,
% 195.44/195.71 ! [ U_101,U_100 ] : ( vplus(U_101, vsucc(U_100)) = vsucc(vplus(U_101, U_100)) & vplus(U_101, v1) = vsucc(U_101) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_40_1]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_40_3, plain,
% 195.44/195.71 ( ! [ U_102 ] : vplus(U_102, v1) = vsucc(U_102) & ! [ U_103,U_100 ] : vplus(U_103, vsucc(U_100)) = vsucc(vplus(U_103, U_100)) ),
% 195.44/195.71 inference(miniscope,[status(thm)],[f_40_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_40_4, plain,
% 195.44/195.71 ( vplus(U_102, v1) = vsucc(U_102) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_40_3]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_40_5, plain,
% 195.44/195.71 ( vplus(U_103, vsucc(U_100)) = vsucc(vplus(U_103, U_100)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_40_3]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_41_1, plain,
% 195.44/195.71 ! [ Vd24 ] : ( Vd24 = v1 | Vd24 = vsucc(vskolem2(Vd24)) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(20, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_41_2, plain,
% 195.44/195.71 ! [ U_104 ] : ( U_104 = v1 | U_104 = vsucc(vskolem2(U_104)) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_41_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_41_3, plain,
% 195.44/195.71 ( U_104 = v1 | U_104 = vsucc(vskolem2(U_104)) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_41_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_42_1, plain,
% 195.44/195.71 ! [ Vd16 ] : ~( vsucc(Vd16) = Vd16 ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(12, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_42_2, plain,
% 195.44/195.71 ! [ U_105 ] : ~( vsucc(U_105) = U_105 ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_42_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_42_3, plain,
% 195.44/195.71 ( vsucc(U_105) != U_105 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_42_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_43_1, plain,
% 195.44/195.71 ! [ Vd7,Vd8 ] : ( Vd7 = Vd8 | ~( vsucc(Vd7) = vsucc(Vd8) ) ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[ass(cond(6, 0), 0)]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_43_2, plain,
% 195.44/195.71 ! [ U_107,U_106 ] : ( U_107 = U_106 | ~( vsucc(U_107) = vsucc(U_106) ) ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_43_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_43_3, plain,
% 195.44/195.71 ( U_107 = U_106 | vsucc(U_107) != vsucc(U_106) ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_43_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_44_1, plain,
% 195.44/195.71 ! [ Vd3,Vd4 ] : ( ~( vsucc(Vd3) = vsucc(Vd4) ) | Vd3 = Vd4 ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[qu(antec(axiom(3)), imp(antec(axiom(3))))]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_44_2, plain,
% 195.44/195.71 ! [ U_109,U_108 ] : ( ~( vsucc(U_109) = vsucc(U_108) ) | U_109 = U_108 ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_44_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_44_3, plain,
% 195.44/195.71 ( vsucc(U_109) != vsucc(U_108) | U_109 = U_108 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_44_2]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_45_1, plain,
% 195.44/195.71 ! [ Vd1 ] : ~( vsucc(Vd1) = v1 ),
% 195.44/195.71 inference(fof_nnf,[status(thm)],[qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))]) ).
% 195.44/195.71
% 195.44/195.71 fof(f_45_2, plain,
% 195.44/195.71 ! [ U_110 ] : ~( vsucc(U_110) = v1 ),
% 195.44/195.71 inference(variable_rename,[status(thm)],[f_45_1]) ).
% 195.44/195.71
% 195.44/195.71 cnf(f_45_3, plain,
% 195.44/195.71 ( vsucc(U_110) != v1 ),
% 195.44/195.71 inference(clausify,[status(thm)],[f_45_2]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_1, axiom,
% 195.44/195.71 ( Eq_x_0 = Eq_x_0 ),
% 195.44/195.71 theory(equality,[reflexivity]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_2, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_x_1 | Eq_x_1 = Eq_x_0 ),
% 195.44/195.71 theory(equality,[symmetry]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_3, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_x_1 | Eq_x_1 != Eq_x_2 | Eq_x_0 = Eq_x_2 ),
% 195.44/195.71 theory(equality,[transitivity]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_4, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | vplus(Eq_x_0, Eq_x_1) = vplus(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_5, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | vsucc(Eq_x_0) = vsucc(Eq_y_0) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_6, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | vskolem2(Eq_x_0) = vskolem2(Eq_y_0) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_7, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | sK1(Eq_x_0, Eq_x_1) = sK1(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_8, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | sK2(Eq_x_0, Eq_x_1) = sK2(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_9, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | sK3(Eq_x_0, Eq_x_1) = sK3(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_10, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | sK4(Eq_x_0, Eq_x_1) = sK4(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_functions]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_11, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | ~greater(Eq_x_0, Eq_x_1) | greater(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_predicates]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_12, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | ~less(Eq_x_0, Eq_x_1) | less(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_predicates]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_13, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | ~leq(Eq_x_0, Eq_x_1) | leq(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_predicates]) ).
% 195.44/195.71
% 195.44/195.71 cnf(equality_14, axiom,
% 195.44/195.71 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | ~geq(Eq_x_0, Eq_x_1) | geq(Eq_y_0, Eq_y_1) ),
% 195.44/195.71 theory(equality,[substitution_predicates]) ).
% 195.44/195.71
% 195.44/195.71 cnf(sat_proved, plain, $false,
% 195.44/195.71 inference(cadical, [status(thm)], [
% 195.58/196.29 ]) ).
% 195.58/196.29 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------