%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : LCL893+1 : TPTP v9.3.1. Released v5.5.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 : n007.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:50:18 AM UTC 2026
% Result : Theorem 204.44s 209.76s
% Output : Proof 206.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL893+1 : TPTP v9.3.1. Released v5.5.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.08/5.36 % Computer : n007.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Sat Sep 19 15:55:25 UTC 2026
% 0.08/5.37 % CPUTime :
% 204.44/209.76 % SZS status Theorem for theBenchmark
% 204.44/209.76 % SZS output start Proof for theBenchmark
% 206.14/211.49 fof(sos_01, axiom,
% 206.14/211.49 ! [ A,B,C ] : +(+(A, B), C) = +(A, +(B, C)),
% 206.14/211.49 file('theBenchmark.p', sos_01) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_02, axiom,
% 206.14/211.49 ! [ A,B ] : +(A, B) = +(B, A),
% 206.14/211.49 file('theBenchmark.p', sos_02) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_03, axiom,
% 206.14/211.49 ! [ A ] : +(A, 0) = A,
% 206.14/211.49 file('theBenchmark.p', sos_03) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_04, axiom,
% 206.14/211.49 ! [ A ] : +(A, 1) = 1,
% 206.14/211.49 file('theBenchmark.p', sos_04) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_05, axiom,
% 206.14/211.49 ! [ A ] : >=(A, A),
% 206.14/211.49 file('theBenchmark.p', sos_05) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_06, axiom,
% 206.14/211.49 ! [ X0,X1,X2 ] : ( ( >=(X0, X1) & >=(X1, X2) ) => >=(X0, X2) ),
% 206.14/211.49 file('theBenchmark.p', sos_06) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_07, axiom,
% 206.14/211.49 ! [ X3,X4 ] : ( ( >=(X3, X4) & >=(X4, X3) ) => X3 = X4 ),
% 206.14/211.49 file('theBenchmark.p', sos_07) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_08, axiom,
% 206.14/211.49 ! [ X5,X6,X7 ] : ( >=(+(X5, X6), X7) <=> >=(X6, ==>(X5, X7)) ),
% 206.14/211.49 file('theBenchmark.p', sos_08) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_09, axiom,
% 206.14/211.49 ! [ A ] : >=(A, 0),
% 206.14/211.49 file('theBenchmark.p', sos_09) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_10, axiom,
% 206.14/211.49 ! [ X8,X9,X10 ] : ( >=(X8, X9) => >=(+(X8, X10), +(X9, X10)) ),
% 206.14/211.49 file('theBenchmark.p', sos_10) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_11, axiom,
% 206.14/211.49 ! [ X11,X12,X13 ] : ( >=(X11, X12) => >=(==>(X12, X13), ==>(X11, X13)) ),
% 206.14/211.49 file('theBenchmark.p', sos_11) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_12, axiom,
% 206.14/211.49 ! [ X14,X15,X16 ] : ( >=(X14, X15) => >=(==>(X16, X14), ==>(X16, X15)) ),
% 206.14/211.49 file('theBenchmark.p', sos_12) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_13, axiom,
% 206.14/211.49 ! [ A,B ] : +(A, ==>(A, B)) = +(B, ==>(B, A)),
% 206.14/211.49 file('theBenchmark.p', sos_13) ).
% 206.14/211.49
% 206.14/211.49 fof(sos_14, axiom,
% 206.14/211.49 ! [ A ] : h(A) = ==>(h(A), A),
% 206.14/211.49 file('theBenchmark.p', sos_14) ).
% 206.14/211.49
% 206.14/211.49 fof(goals_15, conjecture,
% 206.14/211.49 ! [ X17 ] : ( h(X17) = X17 => X17 = 0 ),
% 206.14/211.49 file('theBenchmark.p', goals_15) ).
% 206.14/211.49
% 206.14/211.49 fof(f_1_1, plain,
% 206.14/211.49 ! [ A,B,C ] : +(+(A, B), C) = +(A, +(B, C)),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_01]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_1_2, plain,
% 206.14/211.49 ! [ U_2,U_1,U_0 ] : +(+(U_2, U_1), U_0) = +(U_2, +(U_1, U_0)),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_1_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_1_3, plain,
% 206.14/211.49 ( ( ! [U_0, U_1, U_2] : ( +(+(U_2, U_1), U_0) = +(U_2, +(U_1, U_0)) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_1_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_1_4, plain,
% 206.14/211.49 ( +(+(U_2, U_1), U_0) = +(U_2, +(U_1, U_0)) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_1_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_2_1, plain,
% 206.14/211.49 ! [ A,B ] : +(A, B) = +(B, A),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_02]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_2_2, plain,
% 206.14/211.49 ! [ U_4,U_3 ] : +(U_4, U_3) = +(U_3, U_4),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_2_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_2_3, plain,
% 206.14/211.49 ( ( ! [U_4, U_3] : ( +(U_4, U_3) = +(U_3, U_4) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_2_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_2_4, plain,
% 206.14/211.49 ( +(U_4, U_3) = +(U_3, U_4) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_2_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_3_1, plain,
% 206.14/211.49 ! [ A ] : +(A, 0) = A,
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_03]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_3_2, plain,
% 206.14/211.49 ! [ U_5 ] : +(U_5, 0) = U_5,
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_3_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_3_3, plain,
% 206.14/211.49 ( ( ! [U_5] : ( +(U_5, 0) = U_5 ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_3_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_3_4, plain,
% 206.14/211.49 ( +(U_5, 0) = U_5 ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_3_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_4_1, plain,
% 206.14/211.49 ! [ A ] : +(A, 1) = 1,
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_04]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_4_2, plain,
% 206.14/211.49 ! [ U_6 ] : +(U_6, 1) = 1,
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_4_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_4_3, plain,
% 206.14/211.49 ( ( ! [U_6] : ( +(U_6, 1) = 1 ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_4_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_4_4, plain,
% 206.14/211.49 ( +(U_6, 1) = 1 ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_4_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_5_1, plain,
% 206.14/211.49 ! [ A ] : >=(A, A),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_05]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_5_2, plain,
% 206.14/211.49 ! [ U_7 ] : >=(U_7, U_7),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_5_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_5_3, plain,
% 206.14/211.49 ( ( ! [U_7] : ( >=(U_7, U_7) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_5_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_5_4, plain,
% 206.14/211.49 ( >=(U_7, U_7) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_5_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_6_1, plain,
% 206.14/211.49 ! [ X0,X1,X2 ] : ( ( ~( >=(X0, X1) ) | ~( >=(X1, X2) ) ) | >=(X0, X2) ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_06]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_6_2, plain,
% 206.14/211.49 ! [ U_10,U_9,U_8 ] : ( ( ~( >=(U_10, U_9) ) | ~( >=(U_9, U_8) ) ) | >=(U_10, U_8) ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_6_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_6_3, plain,
% 206.14/211.49 ( ( ! [U_8, U_10, U_9] : ( ~>=(U_10, U_9) | ~>=(U_9, U_8) | >=(U_10, U_8) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_6_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_6_4, plain,
% 206.14/211.49 ( ~>=(U_10, U_9) | ~>=(U_9, U_8) | >=(U_10, U_8) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_6_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_7_1, plain,
% 206.14/211.49 ! [ X3,X4 ] : ( ( ~( >=(X3, X4) ) | ~( >=(X4, X3) ) ) | X3 = X4 ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_07]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_7_2, plain,
% 206.14/211.49 ! [ U_12,U_11 ] : ( ( ~( >=(U_12, U_11) ) | ~( >=(U_11, U_12) ) ) | U_12 = U_11 ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_7_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_7_3, plain,
% 206.14/211.49 ( ( ! [U_12, U_11] : ( ~>=(U_12, U_11) | ~>=(U_11, U_12) | U_12 = U_11 ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_7_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_7_4, plain,
% 206.14/211.49 ( ~>=(U_12, U_11) | ~>=(U_11, U_12) | U_12 = U_11 ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_7_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_8_1, plain,
% 206.14/211.49 ! [ X5,X6,X7 ] : ( ( ~( >=(+(X5, X6), X7) ) | >=(X6, ==>(X5, X7)) ) & ( ~( >=(X6, ==>(X5, X7)) ) | >=(+(X5, X6), X7) ) ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_08]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_8_2, plain,
% 206.14/211.49 ! [ U_15,U_14,U_13 ] : ( ( ~( >=(+(U_15, U_14), U_13) ) | >=(U_14, ==>(U_15, U_13)) ) & ( ~( >=(U_14, ==>(U_15, U_13)) ) | >=(+(U_15, U_14), U_13) ) ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_8_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_8_3, plain,
% 206.14/211.49 ( ! [ U_20,U_18,U_16 ] : ( ~( >=(+(U_20, U_18), U_16) ) | >=(U_18, ==>(U_20, U_16)) ) & ! [ U_21,U_19,U_17 ] : ( ~( >=(U_19, ==>(U_21, U_17)) ) | >=(+(U_21, U_19), U_17) ) ),
% 206.14/211.49 inference(miniscope,[status(thm)],[f_8_2]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_8_4, plain,
% 206.14/211.49 ( ( ! [U_18, U_20, U_16] : ( ~>=(+(U_20, U_18), U_16) | >=(U_18, ==>(U_20, U_16)) ) ) & ( ! [U_17, U_19, U_21] : ( ~>=(U_19, ==>(U_21, U_17)) | >=(+(U_21, U_19), U_17) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_8_3]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_8_5, plain,
% 206.14/211.49 ( ~>=(+(U_20, U_18), U_16) | >=(U_18, ==>(U_20, U_16)) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_8_4]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_8_6, plain,
% 206.14/211.49 ( ~>=(U_19, ==>(U_21, U_17)) | >=(+(U_21, U_19), U_17) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_8_4]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_9_1, plain,
% 206.14/211.49 ! [ A ] : >=(A, 0),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_09]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_9_2, plain,
% 206.14/211.49 ! [ U_22 ] : >=(U_22, 0),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_9_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_9_3, plain,
% 206.14/211.49 ( ( ! [U_22] : ( >=(U_22, 0) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_9_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_9_4, plain,
% 206.14/211.49 ( >=(U_22, 0) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_9_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_10_1, plain,
% 206.14/211.49 ! [ X8,X9,X10 ] : ( ~( >=(X8, X9) ) | >=(+(X8, X10), +(X9, X10)) ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_10]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_10_2, plain,
% 206.14/211.49 ! [ U_25,U_24,U_23 ] : ( ~( >=(U_25, U_24) ) | >=(+(U_25, U_23), +(U_24, U_23)) ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_10_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_10_3, plain,
% 206.14/211.49 ! [ U_25,U_24 ] : ( ~( >=(U_25, U_24) ) | ! [ U_23 ] : >=(+(U_25, U_23), +(U_24, U_23)) ),
% 206.14/211.49 inference(miniscope,[status(thm)],[f_10_2]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_10_4, plain,
% 206.14/211.49 ( ( ! [U_23, U_24, U_25] : ( ~>=(U_25, U_24) | >=(+(U_25, U_23), +(U_24, U_23)) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_10_3]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_10_5, plain,
% 206.14/211.49 ( ~>=(U_25, U_24) | >=(+(U_25, U_23), +(U_24, U_23)) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_10_4]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_11_1, plain,
% 206.14/211.49 ! [ X11,X12,X13 ] : ( ~( >=(X11, X12) ) | >=(==>(X12, X13), ==>(X11, X13)) ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_11]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_11_2, plain,
% 206.14/211.49 ! [ U_28,U_27,U_26 ] : ( ~( >=(U_28, U_27) ) | >=(==>(U_27, U_26), ==>(U_28, U_26)) ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_11_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_11_3, plain,
% 206.14/211.49 ! [ U_28,U_27 ] : ( ~( >=(U_28, U_27) ) | ! [ U_26 ] : >=(==>(U_27, U_26), ==>(U_28, U_26)) ),
% 206.14/211.49 inference(miniscope,[status(thm)],[f_11_2]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_11_4, plain,
% 206.14/211.49 ( ( ! [U_26, U_27, U_28] : ( ~>=(U_28, U_27) | >=(==>(U_27, U_26), ==>(U_28, U_26)) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_11_3]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_11_5, plain,
% 206.14/211.49 ( ~>=(U_28, U_27) | >=(==>(U_27, U_26), ==>(U_28, U_26)) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_11_4]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_12_1, plain,
% 206.14/211.49 ! [ X14,X15,X16 ] : ( ~( >=(X14, X15) ) | >=(==>(X16, X14), ==>(X16, X15)) ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_12]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_12_2, plain,
% 206.14/211.49 ! [ U_31,U_30,U_29 ] : ( ~( >=(U_31, U_30) ) | >=(==>(U_29, U_31), ==>(U_29, U_30)) ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_12_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_12_3, plain,
% 206.14/211.49 ! [ U_31,U_30 ] : ( ~( >=(U_31, U_30) ) | ! [ U_29 ] : >=(==>(U_29, U_31), ==>(U_29, U_30)) ),
% 206.14/211.49 inference(miniscope,[status(thm)],[f_12_2]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_12_4, plain,
% 206.14/211.49 ( ( ! [U_29, U_30, U_31] : ( ~>=(U_31, U_30) | >=(==>(U_29, U_31), ==>(U_29, U_30)) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_12_3]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_12_5, plain,
% 206.14/211.49 ( ~>=(U_31, U_30) | >=(==>(U_29, U_31), ==>(U_29, U_30)) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_12_4]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_13_1, plain,
% 206.14/211.49 ! [ A,B ] : +(A, ==>(A, B)) = +(B, ==>(B, A)),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_13]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_13_2, plain,
% 206.14/211.49 ! [ U_33,U_32 ] : +(U_33, ==>(U_33, U_32)) = +(U_32, ==>(U_32, U_33)),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_13_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_13_3, plain,
% 206.14/211.49 ( ( ! [U_33, U_32] : ( +(U_33, ==>(U_33, U_32)) = +(U_32, ==>(U_32, U_33)) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_13_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_13_4, plain,
% 206.14/211.49 ( +(U_33, ==>(U_33, U_32)) = +(U_32, ==>(U_32, U_33)) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_13_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_14_1, plain,
% 206.14/211.49 ! [ A ] : h(A) = ==>(h(A), A),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[sos_14]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_14_2, plain,
% 206.14/211.49 ! [ U_34 ] : h(U_34) = ==>(h(U_34), U_34),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_14_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_14_3, plain,
% 206.14/211.49 ( ( ! [U_34] : ( h(U_34) = ==>(h(U_34), U_34) ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_14_2]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_14_4, plain,
% 206.14/211.49 ( h(U_34) = ==>(h(U_34), U_34) ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_14_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_15_1, negated_conjecture,
% 206.14/211.49 ~( ! [ X17 ] : ( h(X17) = X17 => X17 = 0 ) ),
% 206.14/211.49 inference(negate,[status(cth)],[goals_15]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_15_2, negated_conjecture,
% 206.14/211.49 ? [ X17 ] : ( h(X17) = X17 & ~( X17 = 0 ) ),
% 206.14/211.49 inference(fof_nnf,[status(thm)],[f_15_1]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_15_3, negated_conjecture,
% 206.14/211.49 ? [ U_35 ] : ( h(U_35) = U_35 & ~( U_35 = 0 ) ),
% 206.14/211.49 inference(variable_rename,[status(thm)],[f_15_2]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_15_4, negated_conjecture,
% 206.14/211.49 ( h(sK1) = sK1 & ~( sK1 = 0 ) ),
% 206.14/211.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_35,sK1)],[f_15_3]) ).
% 206.14/211.49
% 206.14/211.49 fof(f_15_5, negated_conjecture,
% 206.14/211.49 ( ( ( h(sK1) = sK1 ) ) & ( ( sK1 != 0 ) ) ),
% 206.14/211.49 inference(definitional_conversion,[status(esa)],[f_15_4]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_15_6, negated_conjecture,
% 206.14/211.49 ( h(sK1) = sK1 ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_15_5]) ).
% 206.14/211.49
% 206.14/211.49 cnf(f_15_7, negated_conjecture,
% 206.14/211.49 ( sK1 != 0 ),
% 206.14/211.49 inference(clausify,[status(thm)],[f_15_5]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_1, axiom,
% 206.14/211.49 ( Eq_x_0 = Eq_x_0 ),
% 206.14/211.49 theory(equality,[reflexivity]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_2, axiom,
% 206.14/211.49 ( Eq_x_0 != Eq_x_1 | Eq_x_1 = Eq_x_0 ),
% 206.14/211.49 theory(equality,[symmetry]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_3, axiom,
% 206.14/211.49 ( Eq_x_0 != Eq_x_1 | Eq_x_1 != Eq_x_2 | Eq_x_0 = Eq_x_2 ),
% 206.14/211.49 theory(equality,[transitivity]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_4, axiom,
% 206.14/211.49 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | +(Eq_x_0, Eq_x_1) = +(Eq_y_0, Eq_y_1) ),
% 206.14/211.49 theory(equality,[substitution_functions]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_5, axiom,
% 206.14/211.49 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | ==>(Eq_x_0, Eq_x_1) = ==>(Eq_y_0, Eq_y_1) ),
% 206.14/211.49 theory(equality,[substitution_functions]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_6, axiom,
% 206.14/211.49 ( Eq_x_0 != Eq_y_0 | h(Eq_x_0) = h(Eq_y_0) ),
% 206.14/211.49 theory(equality,[substitution_functions]) ).
% 206.14/211.49
% 206.14/211.49 cnf(equality_7, axiom,
% 206.14/211.49 ( Eq_x_0 != Eq_y_0 | Eq_x_1 != Eq_y_1 | ~>=(Eq_x_0, Eq_x_1) | >=(Eq_y_0, Eq_y_1) ),
% 206.14/211.49 theory(equality,[substitution_predicates]) ).
% 206.14/211.49
% 206.14/211.49 cnf(sat_proved, plain, $false,
% 206.14/211.49 inference(cadical, [status(thm)], [
% 206.38/213.13 ]) ).
% 206.38/213.13 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------