%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM845+2 : 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 : n011.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:25 AM UTC 2026
% Result : Theorem 64.34s 64.68s
% Output : Proof 66.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM845+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_PEQ 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.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 19 19:21:26 UTC 2026
% 0.10/0.36 % CPUTime :
% 64.34/64.68 % SZS status Theorem for theBenchmark
% 64.34/64.68 % SZS output start Proof for theBenchmark
% 66.33/66.68 fof(qu(ind(267), imp(267)), conjecture,
% 66.33/66.68 ! [ Vd416 ] : ( vmul(vsucc(vd411), Vd416) = vplus(vmul(vd411, Vd416), Vd416) => vmul(vsucc(vd411), vsucc(Vd416)) = vplus(vmul(vd411, vsucc(Vd416)), vsucc(Vd416)) ),
% 66.33/66.68 file('theBenchmark.p', qu(ind(267), imp(267))) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 0), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vplus(vmul(vd411, Vd413), vd411), vsucc(Vd413)) = vplus(vmul(vd411, vsucc(Vd413)), vsucc(Vd413)) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 0)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 1), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vmul(vd411, Vd413), vplus(vd411, vsucc(Vd413))) = vplus(vplus(vmul(vd411, Vd413), vd411), vsucc(Vd413)) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 1)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 2), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vmul(vd411, Vd413), vsucc(vplus(vd411, Vd413))) = vplus(vmul(vd411, Vd413), vplus(vd411, vsucc(Vd413))) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 2)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 3), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vmul(vd411, Vd413), vplus(vsucc(vd411), Vd413)) = vplus(vmul(vd411, Vd413), vsucc(vplus(vd411, Vd413))) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 3)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 4), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vmul(vd411, Vd413), vplus(Vd413, vsucc(vd411))) = vplus(vmul(vd411, Vd413), vplus(vsucc(vd411), Vd413)) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 4)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 5), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vplus(vmul(vd411, Vd413), Vd413), vsucc(vd411)) = vplus(vmul(vd411, Vd413), vplus(Vd413, vsucc(vd411))) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 5)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 6), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vplus(vmul(vsucc(vd411), Vd413), vsucc(vd411)) = vplus(vplus(vmul(vd411, Vd413), Vd413), vsucc(vd411)) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 6)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(conseq(263), 1), 7), axiom,
% 66.33/66.68 ! [ Vd413 ] : ( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) => vmul(vsucc(vd411), vsucc(Vd413)) = vplus(vmul(vsucc(vd411), Vd413), vsucc(vd411)) ),
% 66.33/66.68 file('theBenchmark.p', ass(cond(conseq(263), 1), 7)) ).
% 66.33/66.68
% 66.33/66.68 fof(holds(264, 412, 2), axiom,
% 66.33/66.68 vsucc(vmul(vd411, v1)) = vplus(vmul(vd411, v1), v1),
% 66.33/66.68 file('theBenchmark.p', holds(264, 412, 2)) ).
% 66.33/66.68
% 66.33/66.68 fof(qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0))), axiom,
% 66.33/66.68 ! [ Vd396,Vd397 ] : ( vmul(Vd396, vsucc(Vd397)) = vplus(vmul(Vd396, Vd397), Vd396) & vmul(Vd396, v1) = Vd396 ),
% 66.33/66.68 file('theBenchmark.p', qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(61, 0), 0), axiom,
% 66.33/66.68 ! [ Vd78,Vd79 ] : vplus(Vd79, Vd78) = vplus(Vd78, Vd79),
% 66.33/66.68 file('theBenchmark.p', ass(cond(61, 0), 0)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(43, 0), 0), axiom,
% 66.33/66.68 ! [ Vd59 ] : vplus(v1, Vd59) = vsucc(Vd59),
% 66.33/66.68 file('theBenchmark.p', ass(cond(43, 0), 0)) ).
% 66.33/66.68
% 66.33/66.68 fof(ass(cond(33, 0), 0), axiom,
% 66.33/66.68 ! [ Vd46,Vd47,Vd48 ] : vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)),
% 66.33/66.68 file('theBenchmark.p', ass(cond(33, 0), 0)) ).
% 66.33/66.68
% 66.33/66.68 fof(qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0))), axiom,
% 66.33/66.68 ! [ Vd42,Vd43 ] : ( vplus(Vd42, vsucc(Vd43)) = vsucc(vplus(Vd42, Vd43)) & vplus(Vd42, v1) = vsucc(Vd42) ),
% 66.33/66.68 file('theBenchmark.p', qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))) ).
% 66.33/66.68
% 66.33/66.68 fof(f_1_1, negated_conjecture,
% 66.33/66.68 ~( ! [ Vd416 ] : ( vmul(vsucc(vd411), Vd416) = vplus(vmul(vd411, Vd416), Vd416) => vmul(vsucc(vd411), vsucc(Vd416)) = vplus(vmul(vd411, vsucc(Vd416)), vsucc(Vd416)) ) ),
% 66.33/66.68 inference(negate,[status(cth)],[qu(ind(267), imp(267))]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_1_2, negated_conjecture,
% 66.33/66.68 ? [ Vd416 ] : ( vmul(vsucc(vd411), Vd416) = vplus(vmul(vd411, Vd416), Vd416) & ~( vmul(vsucc(vd411), vsucc(Vd416)) = vplus(vmul(vd411, vsucc(Vd416)), vsucc(Vd416)) ) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[f_1_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_1_3, negated_conjecture,
% 66.33/66.68 ? [ U_0 ] : ( vmul(vsucc(vd411), U_0) = vplus(vmul(vd411, U_0), U_0) & ~( vmul(vsucc(vd411), vsucc(U_0)) = vplus(vmul(vd411, vsucc(U_0)), vsucc(U_0)) ) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_1_2]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_1_4, negated_conjecture,
% 66.33/66.68 ( vmul(vsucc(vd411), sK1) = vplus(vmul(vd411, sK1), sK1) & ~( vmul(vsucc(vd411), vsucc(sK1)) = vplus(vmul(vd411, vsucc(sK1)), vsucc(sK1)) ) ),
% 66.33/66.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1)],[f_1_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_1_5, negated_conjecture,
% 66.33/66.68 ( ( ( vmul(vsucc(vd411), sK1) = vplus(vmul(vd411, sK1), sK1) ) ) & ( ( vmul(vsucc(vd411), vsucc(sK1)) != vplus(vmul(vd411, vsucc(sK1)), vsucc(sK1)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_1_4]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_1_6, negated_conjecture,
% 66.33/66.68 ( vmul(vsucc(vd411), sK1) = vplus(vmul(vd411, sK1), sK1) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_1_5]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_1_7, negated_conjecture,
% 66.33/66.68 ( vmul(vsucc(vd411), vsucc(sK1)) != vplus(vmul(vd411, vsucc(sK1)), vsucc(sK1)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_1_5]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_2_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vplus(vmul(vd411, Vd413), vd411), vsucc(Vd413)) = vplus(vmul(vd411, vsucc(Vd413)), vsucc(Vd413)) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 0)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_2_2, plain,
% 66.33/66.68 ! [ U_1 ] : ( ~( vmul(vsucc(vd411), U_1) = vplus(vmul(vd411, U_1), U_1) ) | vplus(vplus(vmul(vd411, U_1), vd411), vsucc(U_1)) = vplus(vmul(vd411, vsucc(U_1)), vsucc(U_1)) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_2_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_2_3, plain,
% 66.33/66.68 ( ( ! [U_1] : ( vmul(vsucc(vd411), U_1) != vplus(vmul(vd411, U_1), U_1) | vplus(vplus(vmul(vd411, U_1), vd411), vsucc(U_1)) = vplus(vmul(vd411, vsucc(U_1)), vsucc(U_1)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_2_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_2_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_1) != vplus(vmul(vd411, U_1), U_1) | vplus(vplus(vmul(vd411, U_1), vd411), vsucc(U_1)) = vplus(vmul(vd411, vsucc(U_1)), vsucc(U_1)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_2_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_3_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vmul(vd411, Vd413), vplus(vd411, vsucc(Vd413))) = vplus(vplus(vmul(vd411, Vd413), vd411), vsucc(Vd413)) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 1)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_3_2, plain,
% 66.33/66.68 ! [ U_2 ] : ( ~( vmul(vsucc(vd411), U_2) = vplus(vmul(vd411, U_2), U_2) ) | vplus(vmul(vd411, U_2), vplus(vd411, vsucc(U_2))) = vplus(vplus(vmul(vd411, U_2), vd411), vsucc(U_2)) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_3_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_3_3, plain,
% 66.33/66.68 ( ( ! [U_2] : ( vmul(vsucc(vd411), U_2) != vplus(vmul(vd411, U_2), U_2) | vplus(vmul(vd411, U_2), vplus(vd411, vsucc(U_2))) = vplus(vplus(vmul(vd411, U_2), vd411), vsucc(U_2)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_3_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_3_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_2) != vplus(vmul(vd411, U_2), U_2) | vplus(vmul(vd411, U_2), vplus(vd411, vsucc(U_2))) = vplus(vplus(vmul(vd411, U_2), vd411), vsucc(U_2)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_3_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_4_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vmul(vd411, Vd413), vsucc(vplus(vd411, Vd413))) = vplus(vmul(vd411, Vd413), vplus(vd411, vsucc(Vd413))) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 2)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_4_2, plain,
% 66.33/66.68 ! [ U_3 ] : ( ~( vmul(vsucc(vd411), U_3) = vplus(vmul(vd411, U_3), U_3) ) | vplus(vmul(vd411, U_3), vsucc(vplus(vd411, U_3))) = vplus(vmul(vd411, U_3), vplus(vd411, vsucc(U_3))) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_4_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_4_3, plain,
% 66.33/66.68 ( ( ! [U_3] : ( vmul(vsucc(vd411), U_3) != vplus(vmul(vd411, U_3), U_3) | vplus(vmul(vd411, U_3), vsucc(vplus(vd411, U_3))) = vplus(vmul(vd411, U_3), vplus(vd411, vsucc(U_3))) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_4_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_4_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_3) != vplus(vmul(vd411, U_3), U_3) | vplus(vmul(vd411, U_3), vsucc(vplus(vd411, U_3))) = vplus(vmul(vd411, U_3), vplus(vd411, vsucc(U_3))) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_4_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_5_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vmul(vd411, Vd413), vplus(vsucc(vd411), Vd413)) = vplus(vmul(vd411, Vd413), vsucc(vplus(vd411, Vd413))) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 3)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_5_2, plain,
% 66.33/66.68 ! [ U_4 ] : ( ~( vmul(vsucc(vd411), U_4) = vplus(vmul(vd411, U_4), U_4) ) | vplus(vmul(vd411, U_4), vplus(vsucc(vd411), U_4)) = vplus(vmul(vd411, U_4), vsucc(vplus(vd411, U_4))) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_5_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_5_3, plain,
% 66.33/66.68 ( ( ! [U_4] : ( vmul(vsucc(vd411), U_4) != vplus(vmul(vd411, U_4), U_4) | vplus(vmul(vd411, U_4), vplus(vsucc(vd411), U_4)) = vplus(vmul(vd411, U_4), vsucc(vplus(vd411, U_4))) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_5_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_5_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_4) != vplus(vmul(vd411, U_4), U_4) | vplus(vmul(vd411, U_4), vplus(vsucc(vd411), U_4)) = vplus(vmul(vd411, U_4), vsucc(vplus(vd411, U_4))) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_5_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_6_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vmul(vd411, Vd413), vplus(Vd413, vsucc(vd411))) = vplus(vmul(vd411, Vd413), vplus(vsucc(vd411), Vd413)) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 4)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_6_2, plain,
% 66.33/66.68 ! [ U_5 ] : ( ~( vmul(vsucc(vd411), U_5) = vplus(vmul(vd411, U_5), U_5) ) | vplus(vmul(vd411, U_5), vplus(U_5, vsucc(vd411))) = vplus(vmul(vd411, U_5), vplus(vsucc(vd411), U_5)) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_6_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_6_3, plain,
% 66.33/66.68 ( ( ! [U_5] : ( vmul(vsucc(vd411), U_5) != vplus(vmul(vd411, U_5), U_5) | vplus(vmul(vd411, U_5), vplus(U_5, vsucc(vd411))) = vplus(vmul(vd411, U_5), vplus(vsucc(vd411), U_5)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_6_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_6_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_5) != vplus(vmul(vd411, U_5), U_5) | vplus(vmul(vd411, U_5), vplus(U_5, vsucc(vd411))) = vplus(vmul(vd411, U_5), vplus(vsucc(vd411), U_5)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_6_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_7_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vplus(vmul(vd411, Vd413), Vd413), vsucc(vd411)) = vplus(vmul(vd411, Vd413), vplus(Vd413, vsucc(vd411))) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 5)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_7_2, plain,
% 66.33/66.68 ! [ U_6 ] : ( ~( vmul(vsucc(vd411), U_6) = vplus(vmul(vd411, U_6), U_6) ) | vplus(vplus(vmul(vd411, U_6), U_6), vsucc(vd411)) = vplus(vmul(vd411, U_6), vplus(U_6, vsucc(vd411))) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_7_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_7_3, plain,
% 66.33/66.68 ( ( ! [U_6] : ( vmul(vsucc(vd411), U_6) != vplus(vmul(vd411, U_6), U_6) | vplus(vplus(vmul(vd411, U_6), U_6), vsucc(vd411)) = vplus(vmul(vd411, U_6), vplus(U_6, vsucc(vd411))) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_7_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_7_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_6) != vplus(vmul(vd411, U_6), U_6) | vplus(vplus(vmul(vd411, U_6), U_6), vsucc(vd411)) = vplus(vmul(vd411, U_6), vplus(U_6, vsucc(vd411))) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_7_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_8_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vplus(vmul(vsucc(vd411), Vd413), vsucc(vd411)) = vplus(vplus(vmul(vd411, Vd413), Vd413), vsucc(vd411)) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 6)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_8_2, plain,
% 66.33/66.68 ! [ U_7 ] : ( ~( vmul(vsucc(vd411), U_7) = vplus(vmul(vd411, U_7), U_7) ) | vplus(vmul(vsucc(vd411), U_7), vsucc(vd411)) = vplus(vplus(vmul(vd411, U_7), U_7), vsucc(vd411)) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_8_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_8_3, plain,
% 66.33/66.68 ( ( ! [U_7] : ( vmul(vsucc(vd411), U_7) != vplus(vmul(vd411, U_7), U_7) | vplus(vmul(vsucc(vd411), U_7), vsucc(vd411)) = vplus(vplus(vmul(vd411, U_7), U_7), vsucc(vd411)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_8_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_8_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_7) != vplus(vmul(vd411, U_7), U_7) | vplus(vmul(vsucc(vd411), U_7), vsucc(vd411)) = vplus(vplus(vmul(vd411, U_7), U_7), vsucc(vd411)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_8_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_9_1, plain,
% 66.33/66.68 ! [ Vd413 ] : ( ~( vmul(vsucc(vd411), Vd413) = vplus(vmul(vd411, Vd413), Vd413) ) | vmul(vsucc(vd411), vsucc(Vd413)) = vplus(vmul(vsucc(vd411), Vd413), vsucc(vd411)) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(conseq(263), 1), 7)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_9_2, plain,
% 66.33/66.68 ! [ U_8 ] : ( ~( vmul(vsucc(vd411), U_8) = vplus(vmul(vd411, U_8), U_8) ) | vmul(vsucc(vd411), vsucc(U_8)) = vplus(vmul(vsucc(vd411), U_8), vsucc(vd411)) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_9_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_9_3, plain,
% 66.33/66.68 ( ( ! [U_8] : ( vmul(vsucc(vd411), U_8) != vplus(vmul(vd411, U_8), U_8) | vmul(vsucc(vd411), vsucc(U_8)) = vplus(vmul(vsucc(vd411), U_8), vsucc(vd411)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_9_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_9_4, plain,
% 66.33/66.68 ( vmul(vsucc(vd411), U_8) != vplus(vmul(vd411, U_8), U_8) | vmul(vsucc(vd411), vsucc(U_8)) = vplus(vmul(vsucc(vd411), U_8), vsucc(vd411)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_9_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_10_1, plain,
% 66.33/66.68 vsucc(vmul(vd411, v1)) = vplus(vmul(vd411, v1), v1),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[holds(264, 412, 2)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_10_2, plain,
% 66.33/66.68 ( ( ( vsucc(vmul(vd411, v1)) = vplus(vmul(vd411, v1), v1) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_10_1]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_10_3, plain,
% 66.33/66.68 ( vsucc(vmul(vd411, v1)) = vplus(vmul(vd411, v1), v1) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_10_2]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_11_1, plain,
% 66.33/66.68 ! [ Vd396,Vd397 ] : ( vmul(Vd396, vsucc(Vd397)) = vplus(vmul(Vd396, Vd397), Vd396) & vmul(Vd396, v1) = Vd396 ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_11_2, plain,
% 66.33/66.68 ! [ U_10,U_9 ] : ( vmul(U_10, vsucc(U_9)) = vplus(vmul(U_10, U_9), U_10) & vmul(U_10, v1) = U_10 ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_11_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_11_3, plain,
% 66.33/66.68 ( ! [ U_11 ] : vmul(U_11, v1) = U_11 & ! [ U_12,U_9 ] : vmul(U_12, vsucc(U_9)) = vplus(vmul(U_12, U_9), U_12) ),
% 66.33/66.68 inference(miniscope,[status(thm)],[f_11_2]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_11_4, plain,
% 66.33/66.68 ( ( ! [U_11] : ( vmul(U_11, v1) = U_11 ) ) & ( ! [U_9, U_12] : ( vmul(U_12, vsucc(U_9)) = vplus(vmul(U_12, U_9), U_12) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_11_3]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_11_5, plain,
% 66.33/66.68 ( vmul(U_11, v1) = U_11 ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_11_4]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_11_6, plain,
% 66.33/66.68 ( vmul(U_12, vsucc(U_9)) = vplus(vmul(U_12, U_9), U_12) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_11_4]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_12_1, plain,
% 66.33/66.68 ! [ Vd78,Vd79 ] : vplus(Vd79, Vd78) = vplus(Vd78, Vd79),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(61, 0), 0)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_12_2, plain,
% 66.33/66.68 ! [ U_14,U_13 ] : vplus(U_13, U_14) = vplus(U_14, U_13),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_12_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_12_3, plain,
% 66.33/66.68 ( ( ! [U_13, U_14] : ( vplus(U_13, U_14) = vplus(U_14, U_13) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_12_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_12_4, plain,
% 66.33/66.68 ( vplus(U_13, U_14) = vplus(U_14, U_13) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_12_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_13_1, plain,
% 66.33/66.68 ! [ Vd59 ] : vplus(v1, Vd59) = vsucc(Vd59),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(43, 0), 0)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_13_2, plain,
% 66.33/66.68 ! [ U_15 ] : vplus(v1, U_15) = vsucc(U_15),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_13_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_13_3, plain,
% 66.33/66.68 ( ( ! [U_15] : ( vplus(v1, U_15) = vsucc(U_15) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_13_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_13_4, plain,
% 66.33/66.68 ( vplus(v1, U_15) = vsucc(U_15) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_13_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_14_1, plain,
% 66.33/66.68 ! [ Vd46,Vd47,Vd48 ] : vplus(vplus(Vd46, Vd47), Vd48) = vplus(Vd46, vplus(Vd47, Vd48)),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[ass(cond(33, 0), 0)]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_14_2, plain,
% 66.33/66.68 ! [ U_18,U_17,U_16 ] : vplus(vplus(U_18, U_17), U_16) = vplus(U_18, vplus(U_17, U_16)),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_14_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_14_3, plain,
% 66.33/66.68 ( ( ! [U_16, U_17, U_18] : ( vplus(vplus(U_18, U_17), U_16) = vplus(U_18, vplus(U_17, U_16)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_14_2]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_14_4, plain,
% 66.33/66.68 ( vplus(vplus(U_18, U_17), U_16) = vplus(U_18, vplus(U_17, U_16)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_14_3]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_15_1, plain,
% 66.33/66.68 ! [ Vd42,Vd43 ] : ( vplus(Vd42, vsucc(Vd43)) = vsucc(vplus(Vd42, Vd43)) & vplus(Vd42, v1) = vsucc(Vd42) ),
% 66.33/66.68 inference(fof_nnf,[status(thm)],[qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_15_2, plain,
% 66.33/66.68 ! [ U_20,U_19 ] : ( vplus(U_20, vsucc(U_19)) = vsucc(vplus(U_20, U_19)) & vplus(U_20, v1) = vsucc(U_20) ),
% 66.33/66.68 inference(variable_rename,[status(thm)],[f_15_1]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_15_3, plain,
% 66.33/66.68 ( ! [ U_21 ] : vplus(U_21, v1) = vsucc(U_21) & ! [ U_22,U_19 ] : vplus(U_22, vsucc(U_19)) = vsucc(vplus(U_22, U_19)) ),
% 66.33/66.68 inference(miniscope,[status(thm)],[f_15_2]) ).
% 66.33/66.68
% 66.33/66.68 fof(f_15_4, plain,
% 66.33/66.68 ( ( ! [U_21] : ( vplus(U_21, v1) = vsucc(U_21) ) ) & ( ! [U_19, U_22] : ( vplus(U_22, vsucc(U_19)) = vsucc(vplus(U_22, U_19)) ) ) ),
% 66.33/66.68 inference(definitional_conversion,[status(esa)],[f_15_3]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_15_5, plain,
% 66.33/66.68 ( vplus(U_21, v1) = vsucc(U_21) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_15_4]) ).
% 66.33/66.68
% 66.33/66.68 cnf(f_15_6, plain,
% 66.33/66.68 ( vplus(U_22, vsucc(U_19)) = vsucc(vplus(U_22, U_19)) ),
% 66.33/66.68 inference(clausify,[status(thm)],[f_15_4]) ).
% 66.33/66.68
% 66.33/66.68 cnf(equality_1, axiom,
% 66.33/66.68 ( Eq_x_0 = Eq_x_0 ),
% 66.33/66.68 theory(equality,[reflexivity]) ).
% 66.33/66.68
% 66.33/66.68 cnf(equality_2, axiom,
% 66.33/66.68 ( Eq_x_0 != Eq_x_1 | Eq_x_1 = Eq_x_0 ),
% 66.33/66.68 theory(equality,[symmetry]) ).
% 66.33/66.68
% 66.33/66.68 cnf(equality_3, axiom,
% 66.33/66.68 ( Eq_x_0 != Eq_x_1 | Eq_x_1 != Eq_x_2 | Eq_x_0 = Eq_x_2 ),
% 66.33/66.68 theory(equality,[transitivity]) ).
% 66.33/66.68
% 66.33/66.68 cnf(equality_4, axiom,
% 66.33/66.68 ( Eq_x_0 != Eq_y_0 | vsucc(Eq_x_0) = vsucc(Eq_y_0) ),
% 66.33/66.68 theory(equality,[substitution_functions]) ).
% 66.33/66.68
% 66.33/66.68 cnf(equality_5, axiom,
% 66.33/66.68 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | vmul(Eq_x_0, Eq_x_1) = vmul(Eq_y_0, Eq_y_1) ),
% 66.33/66.68 theory(equality,[substitution_functions]) ).
% 66.33/66.68
% 66.33/66.68 cnf(equality_6, axiom,
% 66.33/66.68 ( 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) ),
% 66.33/66.68 theory(equality,[substitution_functions]) ).
% 66.33/66.68
% 66.33/66.68 cnf(sat_proved, plain, $false,
% 66.33/66.68 inference(cadical, [status(thm)], [
% 66.94/70.44 ]) ).
% 66.94/70.44 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------