%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SYN067+1 : TPTP v8.1.0. Released v2.0.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 : n019.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:07:50 EDT 2022 % Result : Theorem 20.01s 2.93s % Output : CNFRefutation 20.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN067+1 : TPTP v8.1.0. Released v2.0.0. % 0.10/0.12 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jul 11 14:51:38 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.37 # No SInE strategy applied % 0.12/0.37 # Auto-Mode selected heuristic G_E___107_C45_F1_PI_AE_Q7_CS_SP_PS_S0Y % 0.12/0.37 # and selection function SelectMaxLComplexAvoidPosPred. % 0.12/0.37 # % 0.12/0.37 # Presaturation interreduction done % 0.12/0.37 # Number of axioms: 84 Number of unprocessed: 74 % 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 # 74 beginning clauses after preprocessing and clausification % 0.12/0.37 # Creating start rules for all 74 conjectures. % 0.12/0.37 # There are 74 start rule candidates: % 0.12/0.37 # Found 1 unit axioms. % 0.12/0.37 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.12/0.37 # 74 start rule tableaux created. % 0.12/0.37 # 73 extension rule candidate clauses % 0.12/0.37 # 1 unit axiom clauses % 0.12/0.37 % 0.12/0.37 # Requested 8, 32 cores available to the main process. % 20.01/2.93 # There were 36 total branch saturation attempts. % 20.01/2.93 # There were 0 of these attempts blocked. % 20.01/2.93 # There were 0 deferred branch saturation attempts. % 20.01/2.93 # There were 0 free duplicated saturations. % 20.01/2.93 # There were 36 total successful branch saturations. % 20.01/2.93 # There were 0 successful branch saturations in interreduction. % 20.01/2.93 # There were 0 successful branch saturations on the branch. % 20.01/2.93 # There were 36 successful branch saturations after the branch. % 20.01/2.93 # SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.01/2.93 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.01/2.93 # Begin clausification derivation % 20.01/2.93 % 20.01/2.93 # End clausification derivation % 20.01/2.93 # Begin listing active clauses obtained from FOF to CNF conversion % 20.01/2.93 cnf(i_0_84, negated_conjecture, (big_p(a))). % 20.01/2.93 cnf(i_0_67, negated_conjecture, (big_p(esk4_0)|big_p(esk2_0)|~big_p(esk1_0)|~big_p(esk3_0))). % 20.01/2.93 cnf(i_0_66, negated_conjecture, (big_r(esk3_0,esk4_0)|big_p(esk2_0)|~big_p(esk1_0)|~big_p(esk3_0))). % 20.01/2.93 cnf(i_0_55, negated_conjecture, (big_r(esk1_0,esk2_0)|big_p(esk4_0)|~big_p(esk1_0)|~big_p(esk3_0))). % 20.01/2.93 cnf(i_0_54, negated_conjecture, (big_r(esk3_0,esk4_0)|big_r(esk1_0,esk2_0)|~big_p(esk1_0)|~big_p(esk3_0))). % 20.01/2.93 cnf(i_0_43, negated_conjecture, (big_p(esk4_0)|~big_r(esk1_0,X1)|~big_r(X1,X2)|~big_p(esk3_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_42, negated_conjecture, (big_r(esk3_0,esk4_0)|~big_r(esk1_0,X1)|~big_r(X1,X2)|~big_p(esk3_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_63, negated_conjecture, (big_p(esk4_0)|big_p(esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_65, negated_conjecture, (big_p(esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(esk3_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_62, negated_conjecture, (big_r(esk3_0,esk4_0)|big_p(esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_51, negated_conjecture, (big_r(esk1_0,esk2_0)|big_p(esk4_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_53, negated_conjecture, (big_r(esk1_0,esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(esk3_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_50, negated_conjecture, (big_r(esk3_0,esk4_0)|big_r(esk1_0,esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_39, negated_conjecture, (~epred14_0|~epred13_0)). % 20.01/2.93 cnf(i_0_87, negated_conjecture, (epred1_0|big_p(esk7_1(X1))|big_p(X1))). % 20.01/2.93 cnf(i_0_90, negated_conjecture, (epred2_0|big_p(esk5_1(X1))|big_p(X1))). % 20.01/2.93 cnf(i_0_93, negated_conjecture, (epred3_0|big_r(X1,esk8_1(X1))|big_p(X1))). % 20.01/2.93 cnf(i_0_36, negated_conjecture, (~epred2_0|~epred1_0)). % 20.01/2.93 cnf(i_0_35, negated_conjecture, (~epred3_0|~epred2_0)). % 20.01/2.93 cnf(i_0_38, negated_conjecture, (~epred15_0|~epred14_0)). % 20.01/2.93 cnf(i_0_41, negated_conjecture, (~epred16_0|~epred14_0)). % 20.01/2.93 cnf(i_0_61, negated_conjecture, (~epred17_0|~epred14_0)). % 20.01/2.93 cnf(i_0_49, negated_conjecture, (~epred18_0|~epred14_0)). % 20.01/2.93 cnf(i_0_97, negated_conjecture, (epred4_0|big_r(X1,esk6_1(X1))|big_p(X1))). % 20.01/2.93 cnf(i_0_101, negated_conjecture, (epred5_0|big_r(esk8_1(X1),esk7_1(X1))|big_p(X1))). % 20.01/2.93 cnf(i_0_105, negated_conjecture, (epred6_0|big_r(esk6_1(X1),esk5_1(X1))|big_p(X1))). % 20.01/2.93 cnf(i_0_30, negated_conjecture, (~epred4_0|~epred1_0)). % 20.01/2.93 cnf(i_0_34, negated_conjecture, (~epred5_0|~epred2_0)). % 20.01/2.93 cnf(i_0_37, negated_conjecture, (~epred19_0|~epred14_0)). % 20.01/2.93 cnf(i_0_205, negated_conjecture, (epred19_0|~big_r(esk1_0,X1)|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_173, negated_conjecture, (epred16_0|~big_r(esk1_0,X1)|~big_r(X1,X2)|~big_p(esk3_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_24, negated_conjecture, (~epred6_0|~epred1_0)). % 20.01/2.93 cnf(i_0_113, negated_conjecture, (epred7_0|big_p(esk9_1(X1))|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_118, negated_conjecture, (epred8_0|big_p(esk5_1(X1))|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_166, negated_conjecture, (epred14_0|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_29, negated_conjecture, (~epred4_0|~epred3_0)). % 20.01/2.93 cnf(i_0_28, negated_conjecture, (~epred5_0|~epred4_0)). % 20.01/2.93 cnf(i_0_33, negated_conjecture, (~epred7_0|~epred2_0)). % 20.01/2.93 cnf(i_0_18, negated_conjecture, (~epred8_0|~epred1_0)). % 20.01/2.93 cnf(i_0_23, negated_conjecture, (~epred6_0|~epred3_0)). % 20.01/2.93 cnf(i_0_22, negated_conjecture, (~epred6_0|~epred5_0)). % 20.01/2.93 cnf(i_0_163, negated_conjecture, (epred13_0|big_p(esk4_0)|~big_r(esk1_0,X1)|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_169, negated_conjecture, (epred15_0|big_r(esk3_0,esk4_0)|~big_r(esk1_0,X1)|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_185, negated_conjecture, (epred17_0|big_p(esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_32, negated_conjecture, (~epred9_0|~epred2_0)). % 20.01/2.93 cnf(i_0_27, negated_conjecture, (~epred7_0|~epred4_0)). % 20.01/2.93 cnf(i_0_17, negated_conjecture, (~epred8_0|~epred3_0)). % 20.01/2.93 cnf(i_0_12, negated_conjecture, (~epred10_0|~epred1_0)). % 20.01/2.93 cnf(i_0_31, negated_conjecture, (~epred11_0|~epred2_0)). % 20.01/2.93 cnf(i_0_21, negated_conjecture, (~epred7_0|~epred6_0)). % 20.01/2.93 cnf(i_0_125, negated_conjecture, (epred9_0|big_r(X1,esk10_1(X1))|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_133, negated_conjecture, (epred10_0|big_r(X1,esk6_1(X1))|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_189, negated_conjecture, (epred18_0|big_r(esk1_0,esk2_0)|~big_r(esk3_0,X1)|~big_r(X1,X2)|~big_p(esk1_0)|~big_p(X2))). % 20.01/2.93 cnf(i_0_16, negated_conjecture, (~epred8_0|~epred5_0)). % 20.01/2.93 cnf(i_0_6, negated_conjecture, (~epred12_0|~epred1_0)). % 20.01/2.93 cnf(i_0_26, negated_conjecture, (~epred9_0|~epred4_0)). % 20.01/2.93 cnf(i_0_11, negated_conjecture, (~epred10_0|~epred3_0)). % 20.01/2.93 cnf(i_0_15, negated_conjecture, (~epred8_0|~epred7_0)). % 20.01/2.93 cnf(i_0_25, negated_conjecture, (~epred11_0|~epred4_0)). % 20.01/2.93 cnf(i_0_137, negated_conjecture, (epred11_0|big_r(esk10_1(X1),esk9_1(X1))|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_145, negated_conjecture, (epred12_0|big_r(esk6_1(X1),esk5_1(X1))|~big_r(X1,X2)|~big_p(X2))). % 20.01/2.93 cnf(i_0_20, negated_conjecture, (~epred9_0|~epred6_0)). % 20.01/2.93 cnf(i_0_10, negated_conjecture, (~epred10_0|~epred5_0)). % 20.01/2.93 cnf(i_0_5, negated_conjecture, (~epred12_0|~epred3_0)). % 20.01/2.93 cnf(i_0_19, negated_conjecture, (~epred11_0|~epred6_0)). % 20.01/2.93 cnf(i_0_4, negated_conjecture, (~epred12_0|~epred5_0)). % 20.01/2.93 cnf(i_0_14, negated_conjecture, (~epred9_0|~epred8_0)). % 20.01/2.93 cnf(i_0_9, negated_conjecture, (~epred10_0|~epred7_0)). % 20.01/2.93 cnf(i_0_13, negated_conjecture, (~epred11_0|~epred8_0)). % 20.01/2.93 cnf(i_0_3, negated_conjecture, (~epred12_0|~epred7_0)). % 20.01/2.93 cnf(i_0_8, negated_conjecture, (~epred10_0|~epred9_0)). % 20.01/2.93 cnf(i_0_7, negated_conjecture, (~epred11_0|~epred10_0)). % 20.01/2.93 cnf(i_0_2, negated_conjecture, (~epred12_0|~epred9_0)). % 20.01/2.93 cnf(i_0_1, negated_conjecture, (~epred12_0|~epred11_0)). % 20.01/2.93 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 20.01/2.93 # Begin printing tableau % 20.01/2.93 # Found 56 steps % 20.01/2.93 cnf(i_0_8, negated_conjecture, (~epred10_0|~epred9_0), inference(start_rule)). % 20.01/2.93 cnf(i_0_214, plain, (~epred10_0), inference(extension_rule, [i_0_133])). % 20.01/2.93 cnf(i_0_485, plain, (big_r(esk1_0,esk6_1(esk1_0))), inference(extension_rule, [i_0_163])). % 20.01/2.93 cnf(i_0_28012, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_28008, plain, (epred13_0), inference(extension_rule, [i_0_39])). % 20.01/2.93 cnf(i_0_28009, plain, (big_p(esk4_0)), inference(etableau_closure_rule, [i_0_28009, ...])). % 20.01/2.93 cnf(i_0_28011, plain, (~big_r(esk6_1(esk1_0),a)), inference(etableau_closure_rule, [i_0_28011, ...])). % 20.01/2.93 cnf(i_0_28110, plain, (~epred14_0), inference(etableau_closure_rule, [i_0_28110, ...])). % 20.01/2.93 cnf(i_0_486, plain, (~big_r(esk1_0,esk2_0)), inference(extension_rule, [i_0_50])). % 20.01/2.93 cnf(i_0_43774, plain, (~big_r(esk10_1(esk3_0),esk9_1(esk3_0))), inference(extension_rule, [i_0_137])). % 20.01/2.93 cnf(i_0_45035, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_43775, plain, (~big_p(esk1_0)), inference(extension_rule, [i_0_90])). % 20.01/2.93 cnf(i_0_43773, plain, (~big_r(esk3_0,esk10_1(esk3_0))), inference(extension_rule, [i_0_125])). % 20.01/2.93 cnf(i_0_45345, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_43771, plain, (big_r(esk3_0,esk4_0)), inference(extension_rule, [i_0_118])). % 20.01/2.93 cnf(i_0_43776, plain, (~big_p(esk9_1(esk3_0))), inference(extension_rule, [i_0_113])). % 20.01/2.93 cnf(i_0_45473, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_487, plain, (~big_p(esk2_0)), inference(extension_rule, [i_0_62])). % 20.01/2.93 cnf(i_0_45573, plain, (~big_r(esk3_0,esk6_1(esk3_0))), inference(extension_rule, [i_0_133])). % 20.01/2.93 cnf(i_0_47767, plain, (epred10_0), inference(closure_rule, [i_0_214])). % 20.01/2.93 cnf(i_0_47770, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_45571, plain, (big_r(esk3_0,esk4_0)), inference(extension_rule, [i_0_205])). % 20.01/2.93 cnf(i_0_45574, plain, (~big_r(esk6_1(esk3_0),esk5_1(esk3_0))), inference(extension_rule, [i_0_145])). % 20.01/2.93 cnf(i_0_48877, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_45575, plain, (~big_p(esk1_0)), inference(extension_rule, [i_0_97])). % 20.01/2.93 cnf(i_0_45576, plain, (~big_p(esk5_1(esk3_0))), inference(extension_rule, [i_0_101])). % 20.01/2.93 cnf(i_0_215, plain, (~epred9_0), inference(extension_rule, [i_0_125])). % 20.01/2.93 cnf(i_0_49316, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_45032, plain, (epred11_0), inference(etableau_closure_rule, [i_0_45032, ...])). % 20.01/2.93 cnf(i_0_45034, plain, (~big_r(esk3_0,a)), inference(etableau_closure_rule, [i_0_45034, ...])). % 20.01/2.93 cnf(i_0_45182, plain, (epred2_0), inference(etableau_closure_rule, [i_0_45182, ...])). % 20.01/2.93 cnf(i_0_45183, plain, (big_p(esk5_1(esk1_0))), inference(etableau_closure_rule, [i_0_45183, ...])). % 20.01/2.93 cnf(i_0_45342, plain, (epred9_0), inference(etableau_closure_rule, [i_0_45342, ...])). % 20.01/2.93 cnf(i_0_45344, plain, (~big_r(esk3_0,a)), inference(etableau_closure_rule, [i_0_45344, ...])). % 20.01/2.93 cnf(i_0_45406, plain, (epred8_0), inference(etableau_closure_rule, [i_0_45406, ...])). % 20.01/2.93 cnf(i_0_45407, plain, (big_p(esk5_1(esk3_0))), inference(etableau_closure_rule, [i_0_45407, ...])). % 20.01/2.93 cnf(i_0_45409, plain, (~big_p(esk4_0)), inference(etableau_closure_rule, [i_0_45409, ...])). % 20.01/2.93 cnf(i_0_45470, plain, (epred7_0), inference(etableau_closure_rule, [i_0_45470, ...])). % 20.01/2.93 cnf(i_0_45472, plain, (~big_r(esk3_0,a)), inference(etableau_closure_rule, [i_0_45472, ...])). % 20.01/2.93 cnf(i_0_47769, plain, (~big_r(esk3_0,a)), inference(etableau_closure_rule, [i_0_47769, ...])). % 20.01/2.93 cnf(i_0_47833, plain, (epred19_0), inference(etableau_closure_rule, [i_0_47833, ...])). % 20.01/2.93 cnf(i_0_47834, plain, (~big_r(esk1_0,esk3_0)), inference(etableau_closure_rule, [i_0_47834, ...])). % 20.01/2.93 cnf(i_0_47836, plain, (~big_p(esk4_0)), inference(etableau_closure_rule, [i_0_47836, ...])). % 20.01/2.93 cnf(i_0_48874, plain, (epred12_0), inference(etableau_closure_rule, [i_0_48874, ...])). % 20.01/2.93 cnf(i_0_48876, plain, (~big_r(esk3_0,a)), inference(etableau_closure_rule, [i_0_48876, ...])). % 20.01/2.93 cnf(i_0_49012, plain, (epred4_0), inference(etableau_closure_rule, [i_0_49012, ...])). % 20.01/2.93 cnf(i_0_49013, plain, (big_r(esk1_0,esk6_1(esk1_0))), inference(etableau_closure_rule, [i_0_49013, ...])). % 20.01/2.93 cnf(i_0_49149, plain, (epred5_0), inference(etableau_closure_rule, [i_0_49149, ...])). % 20.01/2.93 cnf(i_0_49150, plain, (big_r(esk8_1(esk5_1(esk3_0)),esk7_1(esk5_1(esk3_0)))), inference(etableau_closure_rule, [i_0_49150, ...])). % 20.01/2.93 cnf(i_0_49314, plain, (big_r(esk3_0,esk10_1(esk3_0))), inference(extension_rule, [i_0_53])). % 20.01/2.93 cnf(i_0_57841, plain, (~big_p(a)), inference(closure_rule, [i_0_84])). % 20.01/2.93 cnf(i_0_49315, plain, (~big_r(esk3_0,a)), inference(etableau_closure_rule, [i_0_49315, ...])). % 20.01/2.93 cnf(i_0_57836, plain, (big_r(esk1_0,esk2_0)), inference(etableau_closure_rule, [i_0_57836, ...])). % 20.01/2.93 cnf(i_0_57838, plain, (~big_r(esk10_1(esk3_0),a)), inference(etableau_closure_rule, [i_0_57838, ...])). % 20.01/2.93 cnf(i_0_57839, plain, (~big_p(esk1_0)), inference(etableau_closure_rule, [i_0_57839, ...])). % 20.01/2.93 cnf(i_0_57840, plain, (~big_p(esk3_0)), inference(etableau_closure_rule, [i_0_57840, ...])). % 20.01/2.93 # End printing tableau % 20.01/2.93 # SZS output end % 20.01/2.93 # Branches closed with saturation will be marked with an "s" % 20.01/2.94 # Child (29460) has found a proof. % 20.01/2.94 % 20.01/2.94 # Proof search is over... % 20.01/2.94 # Freeing feature tree %------------------------------------------------------------------------------