%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : PUZ026-1 : TPTP v8.1.0. Released v1.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 : n017.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 : Mon Jul 18 18:10:59 EDT 2022 % Result : Unsatisfiable 2.45s 0.71s % Output : CNFRefutation 2.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : PUZ026-1 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.12 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.11/0.33 % Computer : n017.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Sat May 28 19:12:53 EDT 2022 % 0.11/0.33 % CPUTime : % 0.18/0.35 # No SInE strategy applied % 0.18/0.35 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.18/0.35 # and selection function SelectComplexExceptUniqMaxHorn. % 0.18/0.35 # % 0.18/0.35 # Presaturation interreduction done % 0.18/0.35 # Number of axioms: 23 Number of unprocessed: 23 % 0.18/0.35 # Tableaux proof search. % 0.18/0.35 # APR header successfully linked. % 0.18/0.35 # Hello from C++ % 0.18/0.35 # The folding up rule is enabled... % 0.18/0.35 # Local unification is enabled... % 0.18/0.35 # Any saturation attempts will use folding labels... % 0.18/0.35 # 23 beginning clauses after preprocessing and clausification % 0.18/0.35 # Creating start rules for all 1 conjectures. % 0.18/0.35 # There are 1 start rule candidates: % 0.18/0.35 # Found 6 unit axioms. % 0.18/0.35 # 1 start rule tableaux created. % 0.18/0.35 # 17 extension rule candidate clauses % 0.18/0.35 # 6 unit axiom clauses % 0.18/0.35 % 0.18/0.35 # Requested 8, 32 cores available to the main process. % 0.18/0.35 # There are not enough tableaux to fork, creating more from the initial 1 % 0.18/0.35 # Returning from population with 13 new_tableaux and 0 remaining starting tableaux. % 0.18/0.35 # We now have 13 tableaux to operate on % 2.45/0.71 # There were 56 total branch saturation attempts. % 2.45/0.71 # There were 0 of these attempts blocked. % 2.45/0.71 # There were 0 deferred branch saturation attempts. % 2.45/0.71 # There were 0 free duplicated saturations. % 2.45/0.71 # There were 56 total successful branch saturations. % 2.45/0.71 # There were 10 successful branch saturations in interreduction. % 2.45/0.71 # There were 0 successful branch saturations on the branch. % 2.45/0.71 # There were 46 successful branch saturations after the branch. % 2.45/0.71 # SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.45/0.71 # SZS output start for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.45/0.71 # Begin clausification derivation % 2.45/0.71 % 2.45/0.71 # End clausification derivation % 2.45/0.71 # Begin listing active clauses obtained from FOF to CNF conversion % 2.45/0.71 cnf(i_0_43, hypothesis, (a_truth(says(a,normal(a))))). % 2.45/0.71 cnf(i_0_44, hypothesis, (a_truth(says(b,normal(a))))). % 2.45/0.71 cnf(i_0_45, hypothesis, (a_truth(says(c,not_normal(c))))). % 2.45/0.71 cnf(i_0_40, hypothesis, (people(a,b,c))). % 2.45/0.71 cnf(i_0_41, hypothesis, (people(b,c,a))). % 2.45/0.71 cnf(i_0_42, hypothesis, (people(c,b,a))). % 2.45/0.71 cnf(i_0_26, plain, (~a_truth(truthteller(X1))|~a_truth(liar(X1)))). % 2.45/0.71 cnf(i_0_25, plain, (~a_truth(truthteller(X1))|~a_truth(normal(X1)))). % 2.45/0.71 cnf(i_0_27, plain, (~a_truth(liar(X1))|~a_truth(normal(X1)))). % 2.45/0.71 cnf(i_0_32, plain, (~a_truth(normal(X1))|~a_truth(not_normal(X1)))). % 2.45/0.71 cnf(i_0_46, negated_conjecture, (~a_truth(truthteller(X1))|~a_truth(liar(X2))|~a_truth(normal(X3)))). % 2.45/0.71 cnf(i_0_33, plain, (a_truth(not_normal(X1))|a_truth(normal(X1)))). % 2.45/0.71 cnf(i_0_29, plain, (~a_truth(says(X1,X2))|~a_truth(liar(X1))|~a_truth(X2))). % 2.45/0.71 cnf(i_0_35, plain, (~people(X1,X2,X3)|~a_truth(truthteller(X3))|~a_truth(truthteller(X1)))). % 2.45/0.71 cnf(i_0_34, plain, (~people(X1,X2,X3)|~a_truth(truthteller(X2))|~a_truth(truthteller(X1)))). % 2.45/0.71 cnf(i_0_37, plain, (~people(X1,X2,X3)|~a_truth(liar(X3))|~a_truth(liar(X1)))). % 2.45/0.71 cnf(i_0_24, plain, (a_truth(normal(X1))|a_truth(liar(X1))|a_truth(truthteller(X1)))). % 2.45/0.71 cnf(i_0_28, plain, (a_truth(X1)|~a_truth(says(X2,X1))|~a_truth(truthteller(X2)))). % 2.45/0.71 cnf(i_0_36, plain, (~people(X1,X2,X3)|~a_truth(liar(X2))|~a_truth(liar(X1)))). % 2.45/0.71 cnf(i_0_39, plain, (~people(X1,X2,X3)|~a_truth(normal(X3))|~a_truth(normal(X1)))). % 2.45/0.71 cnf(i_0_38, plain, (~people(X1,X2,X3)|~a_truth(normal(X2))|~a_truth(normal(X1)))). % 2.45/0.71 cnf(i_0_30, plain, (a_truth(normal(X1))|a_truth(truthteller(X1))|~a_truth(says(X1,X2))|~a_truth(X2))). % 2.45/0.71 cnf(i_0_31, plain, (a_truth(normal(X1))|a_truth(liar(X1))|a_truth(X2)|~a_truth(says(X1,X2)))). % 2.45/0.71 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 2.45/0.71 # Begin printing tableau % 2.45/0.71 # Found 134 steps % 2.45/0.71 cnf(i_0_46, negated_conjecture, (~a_truth(truthteller(a))|~a_truth(liar(c))|~a_truth(normal(a))), inference(start_rule)). % 2.45/0.71 cnf(i_0_49, plain, (~a_truth(normal(a))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_172, plain, (~a_truth(says(a,normal(a)))), inference(closure_rule, [i_0_43])). % 2.45/0.71 cnf(i_0_173, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_220, plain, (~a_truth(says(a,truthteller(a)))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_260, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_49])). % 2.45/0.71 cnf(i_0_221, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_286, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_49])). % 2.45/0.71 cnf(i_0_47, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_30])). % 2.45/0.71 cnf(i_0_322, plain, (~a_truth(says(a,normal(a)))), inference(closure_rule, [i_0_43])). % 2.45/0.71 cnf(i_0_320, plain, (a_truth(normal(a))), inference(extension_rule, [i_0_27])). % 2.45/0.71 cnf(i_0_328, plain, (~a_truth(liar(a))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_323, plain, (~a_truth(normal(a))), inference(extension_rule, [i_0_33])). % 2.45/0.71 cnf(i_0_371, plain, (a_truth(not_normal(a))), inference(extension_rule, [i_0_29])). % 2.45/0.71 cnf(i_0_48, plain, (~a_truth(liar(c))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_411, plain, (a_truth(liar(c))), inference(closure_rule, [i_0_48])). % 2.45/0.71 cnf(i_0_412, plain, (~a_truth(says(c,liar(c)))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_500, plain, (~a_truth(says(c,says(c,liar(c))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_542, plain, (a_truth(liar(c))), inference(closure_rule, [i_0_48])). % 2.45/0.71 cnf(i_0_501, plain, (~a_truth(truthteller(c))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_571, plain, (a_truth(liar(c))), inference(closure_rule, [i_0_48])). % 2.45/0.71 cnf(i_0_409, plain, (a_truth(normal(c))), inference(extension_rule, [i_0_32])). % 2.45/0.71 cnf(i_0_576, plain, (~a_truth(not_normal(c))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_614, plain, (~a_truth(says(c,not_normal(c)))), inference(closure_rule, [i_0_45])). % 2.45/0.71 cnf(i_0_261, plain, (a_truth(liar(a))), inference(etableau_closure_rule, [i_0_261, ...])). % 2.45/0.71 cnf(i_0_263, plain, (~a_truth(says(a,says(a,truthteller(a))))), inference(etableau_closure_rule, [i_0_263, ...])). % 2.45/0.71 cnf(i_0_287, plain, (a_truth(liar(a))), inference(etableau_closure_rule, [i_0_287, ...])). % 2.45/0.71 cnf(i_0_541, plain, (a_truth(normal(c))), inference(etableau_closure_rule, [i_0_541, ...])). % 2.45/0.71 cnf(i_0_544, plain, (~a_truth(says(c,says(c,says(c,liar(c)))))), inference(etableau_closure_rule, [i_0_544, ...])). % 2.45/0.71 cnf(i_0_570, plain, (a_truth(normal(c))), inference(etableau_closure_rule, [i_0_570, ...])). % 2.45/0.71 cnf(i_0_615, plain, (~a_truth(truthteller(c))), inference(etableau_closure_rule, [i_0_615, ...])). % 2.45/0.71 cnf(i_0_363, plain, (~a_truth(says(c,liar(a)))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_34001, plain, (~a_truth(says(b,says(c,liar(a))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34047, plain, (~a_truth(says(c,says(b,says(c,liar(a)))))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_34138, plain, (~a_truth(says(c,says(c,says(b,says(c,liar(a))))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34139, plain, (~a_truth(truthteller(c))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_34045, plain, (a_truth(liar(c))), inference(extension_rule, [i_0_26])). % 2.45/0.71 cnf(i_0_34208, plain, (~a_truth(truthteller(c))), inference(extension_rule, [i_0_30])). % 2.45/0.71 cnf(i_0_34240, plain, (~a_truth(says(a,normal(a)))), inference(closure_rule, [i_0_43])). % 2.45/0.71 cnf(i_0_34044, plain, (a_truth(normal(c))), inference(extension_rule, [i_0_39])). % 2.45/0.71 cnf(i_0_34251, plain, (~people(a,b,c)), inference(closure_rule, [i_0_40])). % 2.45/0.71 cnf(i_0_34253, plain, (~a_truth(normal(a))), inference(closure_rule, [i_0_320])). % 2.45/0.71 cnf(i_0_34179, plain, (a_truth(normal(c))), inference(closure_rule, [i_0_34044])). % 2.45/0.71 cnf(i_0_34203, plain, (a_truth(normal(c))), inference(closure_rule, [i_0_34044])). % 2.45/0.71 cnf(i_0_34237, plain, (a_truth(normal(c))), inference(closure_rule, [i_0_34044])). % 2.45/0.71 cnf(i_0_34002, plain, (~a_truth(truthteller(b))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34289, plain, (~a_truth(says(c,truthteller(b)))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34392, plain, (a_truth(normal(b))), inference(extension_rule, [i_0_38])). % 2.45/0.71 cnf(i_0_34406, plain, (~people(a,b,c)), inference(closure_rule, [i_0_40])). % 2.45/0.71 cnf(i_0_34408, plain, (~a_truth(normal(a))), inference(closure_rule, [i_0_320])). % 2.45/0.71 cnf(i_0_34395, plain, (~a_truth(says(b,says(c,truthteller(b))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34450, plain, (a_truth(normal(b))), inference(closure_rule, [i_0_34392])). % 2.45/0.71 cnf(i_0_34393, plain, (a_truth(liar(b))), inference(extension_rule, [i_0_37])). % 2.45/0.71 cnf(i_0_34466, plain, (~a_truth(liar(b))), inference(closure_rule, [i_0_34393])). % 2.45/0.71 cnf(i_0_34286, plain, (a_truth(normal(c))), inference(extension_rule, [i_0_39])). % 2.45/0.71 cnf(i_0_34606, plain, (~people(a,b,c)), inference(closure_rule, [i_0_40])). % 2.45/0.71 cnf(i_0_34608, plain, (~a_truth(normal(a))), inference(closure_rule, [i_0_320])). % 2.45/0.71 cnf(i_0_34287, plain, (a_truth(liar(c))), inference(extension_rule, [i_0_36])). % 2.45/0.71 cnf(i_0_34619, plain, (~people(b,c,a)), inference(closure_rule, [i_0_41])). % 2.45/0.71 cnf(i_0_34621, plain, (~a_truth(liar(b))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_34642, plain, (a_truth(truthteller(b))), inference(closure_rule, [i_0_34002])). % 2.45/0.71 cnf(i_0_364, plain, (~a_truth(truthteller(c))), inference(extension_rule, [i_0_30])). % 2.45/0.71 cnf(i_0_34666, plain, (~a_truth(says(a,normal(a)))), inference(closure_rule, [i_0_43])). % 2.45/0.71 cnf(i_0_34665, plain, (~a_truth(says(c,says(a,normal(a))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34751, plain, (~a_truth(says(c,says(c,says(a,normal(a)))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34862, plain, (a_truth(normal(b))), inference(extension_rule, [i_0_38])). % 2.45/0.71 cnf(i_0_34884, plain, (~people(a,b,c)), inference(closure_rule, [i_0_40])). % 2.45/0.71 cnf(i_0_34886, plain, (~a_truth(normal(a))), inference(closure_rule, [i_0_320])). % 2.45/0.71 cnf(i_0_34865, plain, (~a_truth(says(b,says(c,says(c,says(a,normal(a))))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_34928, plain, (a_truth(normal(b))), inference(closure_rule, [i_0_34862])). % 2.45/0.71 cnf(i_0_34863, plain, (a_truth(liar(b))), inference(extension_rule, [i_0_26])). % 2.45/0.71 cnf(i_0_34748, plain, (a_truth(normal(c))), inference(extension_rule, [i_0_39])). % 2.45/0.71 cnf(i_0_35266, plain, (~people(a,b,c)), inference(closure_rule, [i_0_40])). % 2.45/0.71 cnf(i_0_35268, plain, (~a_truth(normal(a))), inference(closure_rule, [i_0_320])). % 2.45/0.71 cnf(i_0_34749, plain, (a_truth(liar(c))), inference(extension_rule, [i_0_30])). % 2.45/0.71 cnf(i_0_35288, plain, (a_truth(normal(c))), inference(closure_rule, [i_0_34748])). % 2.45/0.71 cnf(i_0_35289, plain, (a_truth(truthteller(c))), inference(closure_rule, [i_0_364])). % 2.45/0.71 cnf(i_0_34182, plain, (~a_truth(says(c,says(c,says(c,says(b,says(c,liar(a)))))))), inference(etableau_closure_rule, [i_0_34182, ...])). % 2.45/0.71 cnf(i_0_34180, plain, (a_truth(liar(c))), inference(etableau_closure_rule, [i_0_34180, ...])). % 2.45/0.71 cnf(i_0_34204, plain, (a_truth(liar(c))), inference(etableau_closure_rule, [i_0_34204, ...])). % 2.45/0.71 cnf(i_0_34239, plain, (~a_truth(says(c,says(a,normal(a))))), inference(etableau_closure_rule, [i_0_34239, ...])). % 2.45/0.71 cnf(i_0_34451, plain, (a_truth(liar(b))), inference(etableau_closure_rule, [i_0_34451, ...])). % 2.45/0.71 cnf(i_0_34453, plain, (~a_truth(says(b,says(b,says(c,truthteller(b)))))), inference(etableau_closure_rule, [i_0_34453, ...])). % 2.45/0.71 cnf(i_0_34464, plain, (~people(b,X9,b)), inference(etableau_closure_rule, [i_0_34464, ...])). % 2.45/0.71 cnf(i_0_34640, plain, (a_truth(normal(b))), inference(etableau_closure_rule, [i_0_34640, ...])). % 2.45/0.71 cnf(i_0_34663, plain, (a_truth(normal(c))), inference(etableau_closure_rule, [i_0_34663, ...])). % 2.45/0.71 cnf(i_0_34929, plain, (a_truth(liar(b))), inference(etableau_closure_rule, [i_0_34929, ...])). % 2.45/0.71 cnf(i_0_34931, plain, (~a_truth(says(b,says(b,says(c,says(c,says(a,normal(a)))))))), inference(etableau_closure_rule, [i_0_34931, ...])). % 2.45/0.71 cnf(i_0_34948, plain, (~a_truth(truthteller(b))), inference(etableau_closure_rule, [i_0_34948, ...])). % 2.45/0.71 cnf(i_0_35290, plain, (~a_truth(says(c,liar(c)))), inference(etableau_closure_rule, [i_0_35290, ...])). % 2.45/0.71 cnf(i_0_379, plain, (~a_truth(says(a,not_normal(a)))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_35520, plain, (~a_truth(says(a,says(a,not_normal(a))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_35545, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_35546, plain, (a_truth(liar(a))), inference(extension_rule, [i_0_37])). % 2.45/0.71 cnf(i_0_44091, plain, (~people(b,c,a)), inference(closure_rule, [i_0_41])). % 2.45/0.71 cnf(i_0_44093, plain, (~a_truth(liar(b))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_44119, plain, (a_truth(liar(b))), inference(closure_rule, [i_0_44093])). % 2.45/0.71 cnf(i_0_35548, plain, (~a_truth(says(a,says(a,says(a,not_normal(a)))))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_44147, plain, (~a_truth(says(a,says(a,says(a,says(a,not_normal(a))))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_44190, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44148, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_44219, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_35521, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_30])). % 2.45/0.71 cnf(i_0_44250, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44253, plain, (~a_truth(says(a,normal(a)))), inference(closure_rule, [i_0_43])). % 2.45/0.71 cnf(i_0_44252, plain, (~a_truth(says(a,says(a,normal(a))))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_44289, plain, (~a_truth(says(a,says(a,says(a,normal(a)))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_44325, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44290, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_44363, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_380, plain, (~a_truth(liar(a))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_44405, plain, (~a_truth(says(a,liar(a)))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_44445, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44446, plain, (a_truth(liar(a))), inference(closure_rule, [i_0_380])). % 2.45/0.71 cnf(i_0_44117, plain, (a_truth(normal(b))), inference(etableau_closure_rule, [i_0_44117, ...])). % 2.45/0.71 cnf(i_0_44120, plain, (~a_truth(says(b,liar(b)))), inference(etableau_closure_rule, [i_0_44120, ...])). % 2.45/0.71 cnf(i_0_44191, plain, (a_truth(liar(a))), inference(etableau_closure_rule, [i_0_44191, ...])). % 2.45/0.71 cnf(i_0_44193, plain, (~a_truth(says(a,says(a,says(a,says(a,says(a,not_normal(a)))))))), inference(etableau_closure_rule, [i_0_44193, ...])). % 2.45/0.71 cnf(i_0_44220, plain, (a_truth(liar(a))), inference(etableau_closure_rule, [i_0_44220, ...])). % 2.45/0.71 cnf(i_0_44326, plain, (a_truth(liar(a))), inference(etableau_closure_rule, [i_0_44326, ...])). % 2.45/0.71 cnf(i_0_44328, plain, (~a_truth(says(a,says(a,says(a,says(a,normal(a))))))), inference(etableau_closure_rule, [i_0_44328, ...])). % 2.45/0.71 cnf(i_0_44364, plain, (a_truth(liar(a))), inference(etableau_closure_rule, [i_0_44364, ...])). % 2.45/0.71 cnf(i_0_44448, plain, (~a_truth(says(a,says(a,liar(a))))), inference(extension_rule, [i_0_28])). % 2.45/0.71 cnf(i_0_44847, plain, (~a_truth(says(a,says(a,says(a,liar(a)))))), inference(extension_rule, [i_0_31])). % 2.45/0.71 cnf(i_0_44890, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44891, plain, (a_truth(liar(a))), inference(closure_rule, [i_0_380])). % 2.45/0.71 cnf(i_0_44848, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_30])). % 2.45/0.71 cnf(i_0_44928, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44931, plain, (~a_truth(says(a,normal(a)))), inference(closure_rule, [i_0_43])). % 2.45/0.71 cnf(i_0_44406, plain, (~a_truth(truthteller(a))), inference(extension_rule, [i_0_24])). % 2.45/0.71 cnf(i_0_44966, plain, (a_truth(normal(a))), inference(closure_rule, [i_0_323])). % 2.45/0.71 cnf(i_0_44967, plain, (a_truth(liar(a))), inference(closure_rule, [i_0_380])). % 2.45/0.71 cnf(i_0_44893, plain, (~a_truth(says(a,says(a,says(a,says(a,liar(a))))))), inference(etableau_closure_rule, [i_0_44893, ...])). % 2.45/0.71 cnf(i_0_44930, plain, (~a_truth(says(a,says(a,normal(a))))), inference(etableau_closure_rule, [i_0_44930, ...])). % 2.45/0.71 # End printing tableau % 2.45/0.71 # SZS output end % 2.45/0.71 # Branches closed with saturation will be marked with an "s" % 3.02/0.72 # Child (24282) has found a proof. % 3.02/0.72 % 3.02/0.72 # Proof search is over... % 3.02/0.72 # Freeing feature tree %------------------------------------------------------------------------------