%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SYN551+1 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 06:12:24 EDT 2022 % Result : Theorem 3.81s 0.88s % Output : CNFRefutation 3.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN551+1 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.07/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.12/0.34 % Computer : n004.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jul 11 22:56:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.37 # No SInE strategy applied % 0.12/0.37 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.12/0.37 # and selection function SelectComplexExceptUniqMaxHorn. % 0.12/0.37 # % 0.12/0.37 # Presaturation interreduction done % 0.12/0.37 # Number of axioms: 13 Number of unprocessed: 13 % 0.12/0.37 # Tableaux proof search. % 0.12/0.37 # APR header successfully linked. % 0.12/0.37 # Hello from C++ % 0.12/0.37 # The folding up rule is enabled... % 0.12/0.37 # Local unification is enabled... % 0.12/0.37 # Any saturation attempts will use folding labels... % 0.12/0.37 # 13 beginning clauses after preprocessing and clausification % 0.12/0.37 # Creating start rules for all 13 conjectures. % 0.12/0.37 # There are 13 start rule candidates: % 0.12/0.37 # Found 0 unit axioms. % 0.12/0.37 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.12/0.37 # 13 start rule tableaux created. % 0.12/0.37 # 13 extension rule candidate clauses % 0.12/0.37 # 0 unit axiom clauses % 0.12/0.37 % 0.12/0.37 # Requested 8, 32 cores available to the main process. % 3.81/0.88 # There were 46 total branch saturation attempts. % 3.81/0.88 # There were 0 of these attempts blocked. % 3.81/0.88 # There were 0 deferred branch saturation attempts. % 3.81/0.88 # There were 0 free duplicated saturations. % 3.81/0.88 # There were 46 total successful branch saturations. % 3.81/0.88 # There were 10 successful branch saturations in interreduction. % 3.81/0.88 # There were 1 successful branch saturations on the branch. % 3.81/0.88 # There were 35 successful branch saturations after the branch. % 3.81/0.88 # SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.81/0.88 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.81/0.88 # Begin clausification derivation % 3.81/0.88 % 3.81/0.88 # End clausification derivation % 3.81/0.88 # Begin listing active clauses obtained from FOF to CNF conversion % 3.81/0.88 cnf(i_0_4, negated_conjecture, (g(f(esk6_0))=esk6_0|f(g(esk5_0))=esk5_0)). % 3.81/0.88 cnf(i_0_5, negated_conjecture, (f(g(X1))!=X1|g(f(X2))!=X2|esk2_0!=esk1_0|esk4_0!=esk3_0)). % 3.81/0.88 cnf(i_0_7, negated_conjecture, (g(f(esk3_0))=esk3_0|f(g(X1))!=X1|g(f(X2))!=X2|esk2_0!=esk1_0)). % 3.81/0.88 cnf(i_0_6, negated_conjecture, (g(f(esk4_0))=esk4_0|f(g(X1))!=X1|g(f(X2))!=X2|esk2_0!=esk1_0)). % 3.81/0.88 cnf(i_0_11, negated_conjecture, (f(g(esk1_0))=esk1_0|f(g(X1))!=X1|g(f(X2))!=X2|esk4_0!=esk3_0)). % 3.81/0.88 cnf(i_0_8, negated_conjecture, (f(g(esk2_0))=esk2_0|f(g(X1))!=X1|g(f(X2))!=X2|esk4_0!=esk3_0)). % 3.81/0.88 cnf(i_0_13, negated_conjecture, (g(f(esk3_0))=esk3_0|f(g(esk1_0))=esk1_0|f(g(X1))!=X1|g(f(X2))!=X2)). % 3.81/0.88 cnf(i_0_2, negated_conjecture, (g(f(esk6_0))=esk6_0|X1=X2|f(g(X2))!=X2|f(g(X1))!=X1)). % 3.81/0.88 cnf(i_0_3, negated_conjecture, (f(g(esk5_0))=esk5_0|X1=X2|g(f(X2))!=X2|g(f(X1))!=X1)). % 3.81/0.88 cnf(i_0_12, negated_conjecture, (g(f(esk4_0))=esk4_0|f(g(esk1_0))=esk1_0|f(g(X1))!=X1|g(f(X2))!=X2)). % 3.81/0.88 cnf(i_0_10, negated_conjecture, (g(f(esk3_0))=esk3_0|f(g(esk2_0))=esk2_0|f(g(X1))!=X1|g(f(X2))!=X2)). % 3.81/0.88 cnf(i_0_9, negated_conjecture, (g(f(esk4_0))=esk4_0|f(g(esk2_0))=esk2_0|f(g(X1))!=X1|g(f(X2))!=X2)). % 3.81/0.88 cnf(i_0_1, negated_conjecture, (X1=X2|X3=X4|f(g(X4))!=X4|f(g(X3))!=X3|g(f(X2))!=X2|g(f(X1))!=X1)). % 3.81/0.88 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 3.81/0.88 # Begin printing tableau % 3.81/0.88 # Found 88 steps % 3.81/0.88 cnf(i_0_7, negated_conjecture, (g(f(esk3_0))=esk3_0|f(g(esk5_0))!=esk5_0|g(f(esk3_0))!=esk3_0|esk2_0!=esk1_0), inference(start_rule)). % 3.81/0.88 cnf(i_0_56, plain, (g(f(esk3_0))=esk3_0), inference(extension_rule, [i_0_3])). % 3.81/0.88 cnf(i_0_12005, plain, (g(f(esk4_0))!=esk4_0), inference(extension_rule, [i_0_9])). % 3.81/0.88 cnf(i_0_17101, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17099, plain, (f(g(esk2_0))=esk2_0), inference(extension_rule, [i_0_11])). % 3.81/0.88 cnf(i_0_17122, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17100, plain, (f(g(esk2_0))!=esk2_0), inference(extension_rule, [i_0_8])). % 3.81/0.88 cnf(i_0_17138, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_12002, plain, (f(g(esk5_0))=esk5_0), inference(extension_rule, [i_0_1])). % 3.81/0.88 cnf(i_0_17163, plain, (f(g(esk5_0))=esk5_0), inference(extension_rule, [i_0_12])). % 3.81/0.88 cnf(i_0_17471, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17167, plain, (g(f(esk4_0))!=esk4_0), inference(extension_rule, [i_0_6])). % 3.81/0.88 cnf(i_0_17491, plain, (f(g(esk5_0))!=esk5_0), inference(closure_rule, [i_0_12002])). % 3.81/0.88 cnf(i_0_17492, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17162, plain, (f(g(esk4_0))=esk4_0), inference(extension_rule, [i_0_2])). % 3.81/0.88 cnf(i_0_17515, plain, (f(g(esk4_0))!=esk4_0), inference(closure_rule, [i_0_17162])). % 3.81/0.88 cnf(i_0_17166, plain, (g(f(f(g(esk4_0))))!=f(g(esk4_0))), inference(extension_rule, [i_0_1])). % 3.81/0.88 cnf(i_0_17550, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17551, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17165, plain, (f(g(f(g(esk5_0))))!=f(g(esk5_0))), inference(extension_rule, [i_0_1])). % 3.81/0.88 cnf(i_0_17600, plain, (f(g(esk5_0))!=esk5_0), inference(closure_rule, [i_0_12002])). % 3.81/0.88 cnf(i_0_17601, plain, (f(g(esk5_0))!=esk5_0), inference(closure_rule, [i_0_12002])). % 3.81/0.88 cnf(i_0_12003, plain, (esk4_0=esk3_0), inference(extension_rule, [i_0_11])). % 3.81/0.88 cnf(i_0_17628, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17626, plain, (f(g(esk1_0))=esk1_0), inference(extension_rule, [i_0_9])). % 3.81/0.88 cnf(i_0_17651, plain, (g(f(esk3_0))!=esk3_0), inference(closure_rule, [i_0_56])). % 3.81/0.88 cnf(i_0_17627, plain, (f(g(esk5_0))!=esk5_0), inference(extension_rule, [i_0_4])). % 3.81/0.88 cnf(i_0_57, plain, (f(g(esk5_0))!=esk5_0), inference(extension_rule, [i_0_3])). % 3.81/0.88 cnf(i_0_17681, plain, (g(f(esk3_0))!=esk3_0), inference(extension_rule, [i_0_10])). % 3.81/0.88 cnf(i_0_17735, plain, (f(g(esk2_0))=esk2_0), inference(extension_rule, [i_0_5])). % 3.81/0.88 cnf(i_0_17736, plain, (f(g(esk2_0))!=esk2_0), inference(extension_rule, [i_0_8])). % 3.81/0.88 cnf(i_0_17737, plain, (g(f(esk3_0))!=esk3_0), inference(extension_rule, [i_0_13])). % 3.81/0.88 cnf(i_0_17680, plain, (g(f(esk4_0))!=esk4_0), inference(extension_rule, [i_0_9])). % 3.81/0.88 cnf(i_0_45665, plain, (f(g(esk2_0))=esk2_0), inference(extension_rule, [i_0_2])). % 3.81/0.88 cnf(i_0_45673, plain, (f(g(esk2_0))!=esk2_0), inference(closure_rule, [i_0_45665])). % 3.81/0.88 cnf(i_0_45666, plain, (f(g(esk5_0))!=esk5_0), inference(extension_rule, [i_0_4])). % 3.81/0.88 cnf(i_0_45667, plain, (g(f(esk3_0))!=esk3_0), inference(extension_rule, [i_0_7])). % 3.81/0.88 cnf(i_0_17679, plain, (esk3_0=esk4_0), inference(extension_rule, [i_0_8])). % 3.81/0.88 cnf(i_0_45680, plain, (f(g(esk2_0))=esk2_0), inference(extension_rule, [i_0_13])). % 3.81/0.88 cnf(i_0_45681, plain, (f(g(esk2_0))!=esk2_0), inference(extension_rule, [i_0_10])). % 3.81/0.88 cnf(i_0_45682, plain, (g(f(esk3_0))!=esk3_0), inference(extension_rule, [i_0_7])). % 3.81/0.88 cnf(i_0_58, plain, (g(f(esk3_0))!=esk3_0), inference(extension_rule, [i_0_13])). % 3.81/0.88 cnf(i_0_59, plain, (esk2_0!=esk1_0), inference(etableau_closure_rule, [i_0_59, ...])). % 3.81/0.88 cnf(i_0_17120, plain, (f(g(esk1_0))=esk1_0), inference(etableau_closure_rule, [i_0_17120, ...])). % 3.81/0.88 cnf(i_0_17123, plain, (esk4_0!=esk3_0), inference(etableau_closure_rule, [i_0_17123, ...])). % 3.81/0.88 cnf(i_0_17137, plain, (f(g(X3))!=X3), inference(etableau_closure_rule, [i_0_17137, ...])). % 3.81/0.88 cnf(i_0_17139, plain, (esk4_0!=esk3_0), inference(etableau_closure_rule, [i_0_17139, ...])). % 3.81/0.88 cnf(i_0_17468, plain, (g(f(esk4_0))=esk4_0), inference(etableau_closure_rule, [i_0_17468, ...])). % 3.81/0.88 cnf(i_0_17469, plain, (f(g(esk1_0))=esk1_0), inference(etableau_closure_rule, [i_0_17469, ...])). % 3.81/0.88 cnf(i_0_17493, plain, (esk2_0!=esk1_0), inference(etableau_closure_rule, [i_0_17493, ...])). % 3.81/0.88 cnf(i_0_17512, plain, (g(f(esk6_0))=esk6_0), inference(etableau_closure_rule, [i_0_17512, ...])). % 3.81/0.88 cnf(i_0_17513, plain, (esk4_0=esk4_0), inference(etableau_closure_rule, [i_0_17513, ...])). % 3.81/0.88 cnf(i_0_17548, plain, (f(g(f(g(esk4_0))))!=f(g(esk4_0))), inference(etableau_closure_rule, [i_0_17548, ...])). % 3.81/0.88 cnf(i_0_17549, plain, (f(g(g(f(f(g(esk4_0))))))!=g(f(f(g(esk4_0))))), inference(etableau_closure_rule, [i_0_17549, ...])). % 3.81/0.88 cnf(i_0_17546, plain, (esk3_0=esk3_0), inference(etableau_closure_rule, [i_0_17546, ...])). % 3.81/0.88 cnf(i_0_17602, plain, (g(f(f(g(esk5_0))))!=f(g(esk5_0))), inference(etableau_closure_rule, [i_0_17602, ...])). % 3.81/0.88 cnf(i_0_17603, plain, (g(f(f(g(f(g(esk5_0))))))!=f(g(f(g(esk5_0))))), inference(etableau_closure_rule, [i_0_17603, ...])). % 3.81/0.88 cnf(i_0_17599, plain, (esk5_0=esk5_0), inference(etableau_closure_rule, [i_0_17599, ...])). % 3.81/0.88 cnf(i_0_17648, plain, (g(f(esk4_0))=esk4_0), inference(etableau_closure_rule, [i_0_17648, ...])). % 3.81/0.88 cnf(i_0_17649, plain, (f(g(esk2_0))=esk2_0), inference(etableau_closure_rule, [i_0_17649, ...])). % 3.81/0.88 cnf(i_0_17664, plain, (g(f(esk6_0))=esk6_0), inference(etableau_closure_rule, [i_0_17664, ...])). % 3.81/0.88 cnf(i_0_17751, plain, (g(f(X8))!=X8), inference(etableau_closure_rule, [i_0_17751, ...])). % 3.81/0.88 cnf(i_0_17752, plain, (esk2_0!=esk1_0), inference(etableau_closure_rule, [i_0_17752, ...])). % 3.81/0.88 cnf(i_0_17753, plain, (esk4_0!=esk3_0), inference(etableau_closure_rule, [i_0_17753, ...])). % 3.81/0.88 cnf(i_0_17763, plain, (f(g(X4))!=X4), inference(etableau_closure_rule, [i_0_17763, ...])). % 3.81/0.88 cnf(i_0_17764, plain, (g(f(X9))!=X9), inference(etableau_closure_rule, [i_0_17764, ...])). % 3.81/0.88 cnf(i_0_17765, plain, (esk4_0!=esk3_0), inference(etableau_closure_rule, [i_0_17765, ...])). % 3.81/0.88 cnf(i_0_17767, plain, (f(g(esk1_0))=esk1_0), inference(etableau_closure_rule, [i_0_17767, ...])). % 3.81/0.88 cnf(i_0_17768, plain, (f(g(X6))!=X6), inference(etableau_closure_rule, [i_0_17768, ...])). % 3.81/0.88 cnf(i_0_17769, plain, (g(f(X10))!=X10), inference(etableau_closure_rule, [i_0_17769, ...])). % 3.81/0.88 cnf(i_0_45670, plain, (g(f(esk6_0))=esk6_0), inference(etableau_closure_rule, [i_0_45670, ...])). % 3.81/0.88 cnf(i_0_45671, plain, (esk2_0=esk2_0), inference(etableau_closure_rule, [i_0_45671, ...])). % 3.81/0.88 cnf(i_0_45674, plain, (g(f(esk6_0))=esk6_0), inference(etableau_closure_rule, [i_0_45674, ...])). % 3.81/0.88 cnf(i_0_45677, plain, (f(g(X5))!=X5), inference(etableau_closure_rule, [i_0_45677, ...])). % 3.81/0.88 cnf(i_0_45678, plain, (g(f(X7))!=X7), inference(etableau_closure_rule, [i_0_45678, ...])). % 3.81/0.88 cnf(i_0_45679, plain, (esk2_0!=esk1_0), inference(etableau_closure_rule, [i_0_45679, ...])). % 3.81/0.88 cnf(i_0_45688, plain, (g(f(esk3_0))=esk3_0), inference(etableau_closure_rule, [i_0_45688, ...])). % 3.81/0.88 cnf(i_0_45689, plain, (f(g(esk1_0))=esk1_0), inference(etableau_closure_rule, [i_0_45689, ...])). % 3.81/0.88 cnf(i_0_45691, plain, (g(f(X14))!=X14), inference(etableau_closure_rule, [i_0_45691, ...])). % 3.81/0.88 cnf(i_0_58780, plain, (g(f(esk3_0))=esk3_0), inference(etableau_closure_rule, [i_0_58780, ...])). % 3.81/0.88 cnf(i_0_58782, plain, (f(g(X13))!=X13), inference(etableau_closure_rule, [i_0_58782, ...])). % 3.81/0.88 cnf(i_0_58783, plain, (g(f(X15))!=X15), inference(etableau_closure_rule, [i_0_58783, ...])). % 3.81/0.88 cnf(i_0_58785, plain, (f(g(X11))!=X11), inference(etableau_closure_rule, [i_0_58785, ...])). % 3.81/0.88 cnf(i_0_58786, plain, (g(f(X16))!=X16), inference(etableau_closure_rule, [i_0_58786, ...])). % 3.81/0.88 cnf(i_0_58787, plain, (esk2_0!=esk1_0), inference(etableau_closure_rule, [i_0_58787, ...])). % 3.81/0.88 cnf(i_0_58789, plain, (f(g(esk1_0))=esk1_0), inference(etableau_closure_rule, [i_0_58789, ...])). % 3.81/0.88 cnf(i_0_58790, plain, (f(g(X12))!=X12), inference(etableau_closure_rule, [i_0_58790, ...])). % 3.81/0.88 cnf(i_0_58791, plain, (g(f(X17))!=X17), inference(etableau_closure_rule, [i_0_58791, ...])). % 3.81/0.88 # End printing tableau % 3.81/0.88 # SZS output end % 3.81/0.88 # Branches closed with saturation will be marked with an "s" % 3.81/0.88 # Child (15623) has found a proof. % 3.81/0.88 % 3.81/0.88 # Proof search is over... % 3.81/0.88 # Freeing feature tree %------------------------------------------------------------------------------