%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : PUZ028-3 : TPTP v8.1.0. Released v1.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 : n023.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 : Satisfiable 0.19s 0.41s % Output : CNFRefutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : PUZ028-3 : TPTP v8.1.0. Released v1.1.0. % 0.07/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 : n023.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 : Sat May 28 22:59:57 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.38 # No SInE strategy applied % 0.19/0.38 # Auto-Mode selected heuristic G_____X1276__C12_02_nc_F1_AE_CS_SP_RG_S04AN % 0.19/0.38 # and selection function SelectComplexExceptUniqMaxHorn. % 0.19/0.38 # % 0.19/0.38 # Presaturation interreduction done % 0.19/0.38 # Number of axioms: 504 Number of unprocessed: 164 % 0.19/0.38 # Tableaux proof search. % 0.19/0.38 # APR header successfully linked. % 0.19/0.38 # Hello from C++ % 0.19/0.39 # The folding up rule is enabled... % 0.19/0.39 # Local unification is enabled... % 0.19/0.39 # Any saturation attempts will use folding labels... % 0.19/0.39 # 164 beginning clauses after preprocessing and clausification % 0.19/0.39 # Creating start rules for all 92 conjectures. % 0.19/0.39 # There are 92 start rule candidates: % 0.19/0.39 # Found 54 unit axioms. % 0.19/0.39 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.19/0.39 # 92 start rule tableaux created. % 0.19/0.39 # 110 extension rule candidate clauses % 0.19/0.39 # 54 unit axiom clauses % 0.19/0.39 % 0.19/0.39 # Requested 8, 32 cores available to the main process. % 0.19/0.40 # 24236 Satisfiable branch % 0.19/0.41 # Satisfiable branch found. % 0.19/0.41 # There were 1 total branch saturation attempts. % 0.19/0.41 # There were 0 of these attempts blocked. % 0.19/0.41 # There were 0 deferred branch saturation attempts. % 0.19/0.41 # There were 0 free duplicated saturations. % 0.19/0.41 # There were 0 total successful branch saturations. % 0.19/0.41 # There were 0 successful branch saturations in interreduction. % 0.19/0.41 # There were 0 successful branch saturations on the branch. % 0.19/0.41 # There were 0 successful branch saturations after the branch. % 0.19/0.41 # SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.41 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.41 # Begin clausification derivation % 0.19/0.41 % 0.19/0.41 # End clausification derivation % 0.19/0.41 # Begin listing active clauses obtained from FOF to CNF conversion % 0.19/0.41 cnf(i_0_505, plain, (person(n1))). % 0.19/0.41 cnf(i_0_506, plain, (person(n2))). % 0.19/0.41 cnf(i_0_507, plain, (person(n3))). % 0.19/0.41 cnf(i_0_508, plain, (person(n4))). % 0.19/0.41 cnf(i_0_509, plain, (person(n5))). % 0.19/0.41 cnf(i_0_510, plain, (person(n6))). % 0.19/0.41 cnf(i_0_511, plain, (not_equal(n1,n2))). % 0.19/0.41 cnf(i_0_512, plain, (not_equal(n1,n3))). % 0.19/0.41 cnf(i_0_513, plain, (not_equal(n1,n4))). % 0.19/0.41 cnf(i_0_514, plain, (not_equal(n1,n5))). % 0.19/0.41 cnf(i_0_515, plain, (not_equal(n1,n6))). % 0.19/0.41 cnf(i_0_516, plain, (not_equal(n2,n1))). % 0.19/0.41 cnf(i_0_517, plain, (not_equal(n2,n3))). % 0.19/0.41 cnf(i_0_518, plain, (not_equal(n2,n4))). % 0.19/0.41 cnf(i_0_519, plain, (not_equal(n2,n5))). % 0.19/0.41 cnf(i_0_520, plain, (not_equal(n2,n6))). % 0.19/0.41 cnf(i_0_521, plain, (not_equal(n3,n1))). % 0.19/0.41 cnf(i_0_522, plain, (not_equal(n3,n2))). % 0.19/0.41 cnf(i_0_523, plain, (not_equal(n3,n4))). % 0.19/0.41 cnf(i_0_524, plain, (not_equal(n3,n5))). % 0.19/0.41 cnf(i_0_525, plain, (not_equal(n3,n6))). % 0.19/0.41 cnf(i_0_526, plain, (not_equal(n4,n1))). % 0.19/0.41 cnf(i_0_527, plain, (not_equal(n4,n2))). % 0.19/0.41 cnf(i_0_528, plain, (not_equal(n4,n3))). % 0.19/0.41 cnf(i_0_529, plain, (not_equal(n4,n5))). % 0.19/0.41 cnf(i_0_530, plain, (not_equal(n4,n6))). % 0.19/0.41 cnf(i_0_531, plain, (not_equal(n5,n1))). % 0.19/0.41 cnf(i_0_532, plain, (not_equal(n5,n2))). % 0.19/0.41 cnf(i_0_533, plain, (not_equal(n5,n3))). % 0.19/0.41 cnf(i_0_534, plain, (not_equal(n5,n4))). % 0.19/0.41 cnf(i_0_535, plain, (not_equal(n5,n6))). % 0.19/0.41 cnf(i_0_536, plain, (not_equal(n6,n1))). % 0.19/0.41 cnf(i_0_537, plain, (not_equal(n6,n2))). % 0.19/0.41 cnf(i_0_538, plain, (not_equal(n6,n3))). % 0.19/0.41 cnf(i_0_539, plain, (not_equal(n6,n4))). % 0.19/0.41 cnf(i_0_540, plain, (not_equal(n6,n5))). % 0.19/0.41 cnf(i_0_577, negated_conjecture, (~familiar(n1,n1))). % 0.19/0.41 cnf(i_0_620, negated_conjecture, (~familiar(n2,n2))). % 0.19/0.41 cnf(i_0_663, negated_conjecture, (~familiar(n3,n3))). % 0.19/0.41 cnf(i_0_706, negated_conjecture, (~familiar(n4,n4))). % 0.19/0.41 cnf(i_0_749, negated_conjecture, (~familiar(n5,n5))). % 0.19/0.41 cnf(i_0_792, negated_conjecture, (~familiar(n6,n6))). % 0.19/0.41 cnf(i_0_793, negated_conjecture, (~not_familiar(n1,n1))). % 0.19/0.41 cnf(i_0_836, negated_conjecture, (~not_familiar(n2,n2))). % 0.19/0.41 cnf(i_0_879, negated_conjecture, (~not_familiar(n3,n3))). % 0.19/0.41 cnf(i_0_922, negated_conjecture, (~not_familiar(n4,n4))). % 0.19/0.41 cnf(i_0_965, negated_conjecture, (~not_familiar(n5,n5))). % 0.19/0.41 cnf(i_0_1008, negated_conjecture, (~not_familiar(n6,n6))). % 0.19/0.41 cnf(i_0_541, plain, (~not_equal(n1,n1))). % 0.19/0.41 cnf(i_0_548, plain, (~not_equal(n2,n2))). % 0.19/0.41 cnf(i_0_555, plain, (~not_equal(n3,n3))). % 0.19/0.41 cnf(i_0_562, plain, (~not_equal(n4,n4))). % 0.19/0.41 cnf(i_0_569, plain, (~not_equal(n5,n5))). % 0.19/0.41 cnf(i_0_576, plain, (~not_equal(n6,n6))). % 0.19/0.41 cnf(i_0_585, negated_conjecture, (~familiar(n1,n2)|~familiar(n2,n3)|~familiar(n3,n1))). % 0.19/0.41 cnf(i_0_586, negated_conjecture, (~familiar(n1,n2)|~familiar(n2,n4)|~familiar(n4,n1))). % 0.19/0.41 cnf(i_0_587, negated_conjecture, (~familiar(n1,n2)|~familiar(n2,n5)|~familiar(n5,n1))). % 0.19/0.41 cnf(i_0_588, negated_conjecture, (~familiar(n1,n2)|~familiar(n2,n6)|~familiar(n6,n1))). % 0.19/0.41 cnf(i_0_590, negated_conjecture, (~familiar(n1,n3)|~familiar(n2,n1)|~familiar(n3,n2))). % 0.19/0.41 cnf(i_0_592, negated_conjecture, (~familiar(n1,n3)|~familiar(n3,n4)|~familiar(n4,n1))). % 0.19/0.41 cnf(i_0_593, negated_conjecture, (~familiar(n1,n3)|~familiar(n3,n5)|~familiar(n5,n1))). % 0.19/0.41 cnf(i_0_594, negated_conjecture, (~familiar(n1,n3)|~familiar(n3,n6)|~familiar(n6,n1))). % 0.19/0.41 cnf(i_0_596, negated_conjecture, (~familiar(n1,n4)|~familiar(n2,n1)|~familiar(n4,n2))). % 0.19/0.41 cnf(i_0_597, negated_conjecture, (~familiar(n1,n4)|~familiar(n3,n1)|~familiar(n4,n3))). % 0.19/0.41 cnf(i_0_599, negated_conjecture, (~familiar(n1,n4)|~familiar(n4,n5)|~familiar(n5,n1))). % 0.19/0.41 cnf(i_0_600, negated_conjecture, (~familiar(n1,n4)|~familiar(n4,n6)|~familiar(n6,n1))). % 0.19/0.41 cnf(i_0_602, negated_conjecture, (~familiar(n1,n5)|~familiar(n2,n1)|~familiar(n5,n2))). % 0.19/0.41 cnf(i_0_603, negated_conjecture, (~familiar(n1,n5)|~familiar(n3,n1)|~familiar(n5,n3))). % 0.19/0.41 cnf(i_0_604, negated_conjecture, (~familiar(n1,n5)|~familiar(n4,n1)|~familiar(n5,n4))). % 0.19/0.41 cnf(i_0_606, negated_conjecture, (~familiar(n1,n5)|~familiar(n5,n6)|~familiar(n6,n1))). % 0.19/0.41 cnf(i_0_608, negated_conjecture, (~familiar(n1,n6)|~familiar(n2,n1)|~familiar(n6,n2))). % 0.19/0.41 cnf(i_0_609, negated_conjecture, (~familiar(n1,n6)|~familiar(n3,n1)|~familiar(n6,n3))). % 0.19/0.41 cnf(i_0_610, negated_conjecture, (~familiar(n1,n6)|~familiar(n4,n1)|~familiar(n6,n4))). % 0.19/0.41 cnf(i_0_611, negated_conjecture, (~familiar(n1,n6)|~familiar(n5,n1)|~familiar(n6,n5))). % 0.19/0.41 cnf(i_0_628, negated_conjecture, (~familiar(n2,n3)|~familiar(n3,n4)|~familiar(n4,n2))). % 0.19/0.41 cnf(i_0_629, negated_conjecture, (~familiar(n2,n3)|~familiar(n3,n5)|~familiar(n5,n2))). % 0.19/0.41 cnf(i_0_630, negated_conjecture, (~familiar(n2,n3)|~familiar(n3,n6)|~familiar(n6,n2))). % 0.19/0.41 cnf(i_0_633, negated_conjecture, (~familiar(n2,n4)|~familiar(n3,n2)|~familiar(n4,n3))). % 0.19/0.41 cnf(i_0_635, negated_conjecture, (~familiar(n2,n4)|~familiar(n4,n5)|~familiar(n5,n2))). % 0.19/0.41 cnf(i_0_636, negated_conjecture, (~familiar(n2,n4)|~familiar(n4,n6)|~familiar(n6,n2))). % 0.19/0.41 cnf(i_0_639, negated_conjecture, (~familiar(n2,n5)|~familiar(n3,n2)|~familiar(n5,n3))). % 0.19/0.41 cnf(i_0_640, negated_conjecture, (~familiar(n2,n5)|~familiar(n4,n2)|~familiar(n5,n4))). % 0.19/0.41 cnf(i_0_642, negated_conjecture, (~familiar(n2,n5)|~familiar(n5,n6)|~familiar(n6,n2))). % 0.19/0.41 cnf(i_0_645, negated_conjecture, (~familiar(n2,n6)|~familiar(n3,n2)|~familiar(n6,n3))). % 0.19/0.41 cnf(i_0_646, negated_conjecture, (~familiar(n2,n6)|~familiar(n4,n2)|~familiar(n6,n4))). % 0.19/0.41 cnf(i_0_647, negated_conjecture, (~familiar(n2,n6)|~familiar(n5,n2)|~familiar(n6,n5))). % 0.19/0.41 cnf(i_0_671, negated_conjecture, (~familiar(n3,n4)|~familiar(n4,n5)|~familiar(n5,n3))). % 0.19/0.41 cnf(i_0_672, negated_conjecture, (~familiar(n3,n4)|~familiar(n4,n6)|~familiar(n6,n3))). % 0.19/0.41 cnf(i_0_676, negated_conjecture, (~familiar(n3,n5)|~familiar(n4,n3)|~familiar(n5,n4))). % 0.19/0.41 cnf(i_0_678, negated_conjecture, (~familiar(n3,n5)|~familiar(n5,n6)|~familiar(n6,n3))). % 0.19/0.41 cnf(i_0_682, negated_conjecture, (~familiar(n3,n6)|~familiar(n4,n3)|~familiar(n6,n4))). % 0.19/0.41 cnf(i_0_683, negated_conjecture, (~familiar(n3,n6)|~familiar(n5,n3)|~familiar(n6,n5))). % 0.19/0.41 cnf(i_0_714, negated_conjecture, (~familiar(n4,n5)|~familiar(n5,n6)|~familiar(n6,n4))). % 0.19/0.41 cnf(i_0_719, negated_conjecture, (~familiar(n4,n6)|~familiar(n5,n4)|~familiar(n6,n5))). % 0.19/0.41 cnf(i_0_542, plain, (not_familiar(n1,n2)|familiar(n1,n2))). % 0.19/0.41 cnf(i_0_801, negated_conjecture, (~not_familiar(n1,n2)|~not_familiar(n2,n3)|~not_familiar(n3,n1))). % 0.19/0.41 cnf(i_0_802, negated_conjecture, (~not_familiar(n1,n2)|~not_familiar(n2,n4)|~not_familiar(n4,n1))). % 0.19/0.41 cnf(i_0_803, negated_conjecture, (~not_familiar(n1,n2)|~not_familiar(n2,n5)|~not_familiar(n5,n1))). % 0.19/0.41 cnf(i_0_804, negated_conjecture, (~not_familiar(n1,n2)|~not_familiar(n2,n6)|~not_familiar(n6,n1))). % 0.19/0.41 cnf(i_0_806, negated_conjecture, (~not_familiar(n1,n3)|~not_familiar(n2,n1)|~not_familiar(n3,n2))). % 0.19/0.41 cnf(i_0_808, negated_conjecture, (~not_familiar(n1,n3)|~not_familiar(n3,n4)|~not_familiar(n4,n1))). % 0.19/0.41 cnf(i_0_809, negated_conjecture, (~not_familiar(n1,n3)|~not_familiar(n3,n5)|~not_familiar(n5,n1))). % 0.19/0.41 cnf(i_0_543, plain, (not_familiar(n1,n3)|familiar(n1,n3))). % 0.19/0.41 cnf(i_0_810, negated_conjecture, (~not_familiar(n1,n3)|~not_familiar(n3,n6)|~not_familiar(n6,n1))). % 0.19/0.41 cnf(i_0_812, negated_conjecture, (~not_familiar(n1,n4)|~not_familiar(n2,n1)|~not_familiar(n4,n2))). % 0.19/0.41 cnf(i_0_813, negated_conjecture, (~not_familiar(n1,n4)|~not_familiar(n3,n1)|~not_familiar(n4,n3))). % 0.19/0.41 cnf(i_0_815, negated_conjecture, (~not_familiar(n1,n4)|~not_familiar(n4,n5)|~not_familiar(n5,n1))). % 0.19/0.41 cnf(i_0_816, negated_conjecture, (~not_familiar(n1,n4)|~not_familiar(n4,n6)|~not_familiar(n6,n1))). % 0.19/0.41 cnf(i_0_818, negated_conjecture, (~not_familiar(n1,n5)|~not_familiar(n2,n1)|~not_familiar(n5,n2))). % 0.19/0.41 cnf(i_0_819, negated_conjecture, (~not_familiar(n1,n5)|~not_familiar(n3,n1)|~not_familiar(n5,n3))). % 0.19/0.41 cnf(i_0_544, plain, (not_familiar(n1,n4)|familiar(n1,n4))). % 0.19/0.41 cnf(i_0_820, negated_conjecture, (~not_familiar(n1,n5)|~not_familiar(n4,n1)|~not_familiar(n5,n4))). % 0.19/0.41 cnf(i_0_822, negated_conjecture, (~not_familiar(n1,n5)|~not_familiar(n5,n6)|~not_familiar(n6,n1))). % 0.19/0.41 cnf(i_0_824, negated_conjecture, (~not_familiar(n1,n6)|~not_familiar(n2,n1)|~not_familiar(n6,n2))). % 0.19/0.41 cnf(i_0_825, negated_conjecture, (~not_familiar(n1,n6)|~not_familiar(n3,n1)|~not_familiar(n6,n3))). % 0.19/0.41 cnf(i_0_826, negated_conjecture, (~not_familiar(n1,n6)|~not_familiar(n4,n1)|~not_familiar(n6,n4))). % 0.19/0.41 cnf(i_0_827, negated_conjecture, (~not_familiar(n1,n6)|~not_familiar(n5,n1)|~not_familiar(n6,n5))). % 0.19/0.41 cnf(i_0_545, plain, (not_familiar(n1,n5)|familiar(n1,n5))). % 0.19/0.41 cnf(i_0_844, negated_conjecture, (~not_familiar(n2,n3)|~not_familiar(n3,n4)|~not_familiar(n4,n2))). % 0.19/0.41 cnf(i_0_845, negated_conjecture, (~not_familiar(n2,n3)|~not_familiar(n3,n5)|~not_familiar(n5,n2))). % 0.19/0.41 cnf(i_0_846, negated_conjecture, (~not_familiar(n2,n3)|~not_familiar(n3,n6)|~not_familiar(n6,n2))). % 0.19/0.41 cnf(i_0_849, negated_conjecture, (~not_familiar(n2,n4)|~not_familiar(n3,n2)|~not_familiar(n4,n3))). % 0.19/0.41 cnf(i_0_851, negated_conjecture, (~not_familiar(n2,n4)|~not_familiar(n4,n5)|~not_familiar(n5,n2))). % 0.19/0.41 cnf(i_0_852, negated_conjecture, (~not_familiar(n2,n4)|~not_familiar(n4,n6)|~not_familiar(n6,n2))). % 0.19/0.41 cnf(i_0_855, negated_conjecture, (~not_familiar(n2,n5)|~not_familiar(n3,n2)|~not_familiar(n5,n3))). % 0.19/0.41 cnf(i_0_546, plain, (not_familiar(n1,n6)|familiar(n1,n6))). % 0.19/0.41 cnf(i_0_856, negated_conjecture, (~not_familiar(n2,n5)|~not_familiar(n4,n2)|~not_familiar(n5,n4))). % 0.19/0.41 cnf(i_0_858, negated_conjecture, (~not_familiar(n2,n5)|~not_familiar(n5,n6)|~not_familiar(n6,n2))). % 0.19/0.41 cnf(i_0_861, negated_conjecture, (~not_familiar(n2,n6)|~not_familiar(n3,n2)|~not_familiar(n6,n3))). % 0.19/0.41 cnf(i_0_862, negated_conjecture, (~not_familiar(n2,n6)|~not_familiar(n4,n2)|~not_familiar(n6,n4))). % 0.19/0.41 cnf(i_0_863, negated_conjecture, (~not_familiar(n2,n6)|~not_familiar(n5,n2)|~not_familiar(n6,n5))). % 0.19/0.41 cnf(i_0_887, negated_conjecture, (~not_familiar(n3,n4)|~not_familiar(n4,n5)|~not_familiar(n5,n3))). % 0.19/0.41 cnf(i_0_888, negated_conjecture, (~not_familiar(n3,n4)|~not_familiar(n4,n6)|~not_familiar(n6,n3))). % 0.19/0.41 cnf(i_0_547, plain, (not_familiar(n2,n1)|familiar(n2,n1))). % 0.19/0.41 cnf(i_0_892, negated_conjecture, (~not_familiar(n3,n5)|~not_familiar(n4,n3)|~not_familiar(n5,n4))). % 0.19/0.41 cnf(i_0_894, negated_conjecture, (~not_familiar(n3,n5)|~not_familiar(n5,n6)|~not_familiar(n6,n3))). % 0.19/0.41 cnf(i_0_898, negated_conjecture, (~not_familiar(n3,n6)|~not_familiar(n4,n3)|~not_familiar(n6,n4))). % 0.19/0.41 cnf(i_0_899, negated_conjecture, (~not_familiar(n3,n6)|~not_familiar(n5,n3)|~not_familiar(n6,n5))). % 0.19/0.41 cnf(i_0_930, negated_conjecture, (~not_familiar(n4,n5)|~not_familiar(n5,n6)|~not_familiar(n6,n4))). % 0.19/0.41 cnf(i_0_935, negated_conjecture, (~not_familiar(n4,n6)|~not_familiar(n5,n4)|~not_familiar(n6,n5))). % 0.19/0.41 cnf(i_0_549, plain, (not_familiar(n2,n3)|familiar(n2,n3))). % 0.19/0.41 cnf(i_0_550, plain, (not_familiar(n2,n4)|familiar(n2,n4))). % 0.19/0.41 cnf(i_0_551, plain, (not_familiar(n2,n5)|familiar(n2,n5))). % 0.19/0.41 cnf(i_0_552, plain, (not_familiar(n2,n6)|familiar(n2,n6))). % 0.19/0.41 cnf(i_0_553, plain, (not_familiar(n3,n1)|familiar(n3,n1))). % 0.19/0.41 cnf(i_0_554, plain, (not_familiar(n3,n2)|familiar(n3,n2))). % 0.19/0.41 cnf(i_0_556, plain, (not_familiar(n3,n4)|familiar(n3,n4))). % 0.19/0.41 cnf(i_0_557, plain, (not_familiar(n3,n5)|familiar(n3,n5))). % 0.19/0.41 cnf(i_0_558, plain, (not_familiar(n3,n6)|familiar(n3,n6))). % 0.19/0.41 cnf(i_0_559, plain, (not_familiar(n4,n1)|familiar(n4,n1))). % 0.19/0.41 cnf(i_0_560, plain, (not_familiar(n4,n2)|familiar(n4,n2))). % 0.19/0.41 cnf(i_0_561, plain, (not_familiar(n4,n3)|familiar(n4,n3))). % 0.19/0.41 cnf(i_0_563, plain, (not_familiar(n4,n5)|familiar(n4,n5))). % 0.19/0.41 cnf(i_0_564, plain, (not_familiar(n4,n6)|familiar(n4,n6))). % 0.19/0.41 cnf(i_0_565, plain, (not_familiar(n5,n1)|familiar(n5,n1))). % 0.19/0.41 cnf(i_0_566, plain, (not_familiar(n5,n2)|familiar(n5,n2))). % 0.19/0.41 cnf(i_0_567, plain, (not_familiar(n5,n3)|familiar(n5,n3))). % 0.19/0.41 cnf(i_0_568, plain, (not_familiar(n5,n4)|familiar(n5,n4))). % 0.19/0.41 cnf(i_0_570, plain, (not_familiar(n5,n6)|familiar(n5,n6))). % 0.19/0.41 cnf(i_0_571, plain, (not_familiar(n6,n1)|familiar(n6,n1))). % 0.19/0.41 cnf(i_0_572, plain, (not_familiar(n6,n2)|familiar(n6,n2))). % 0.19/0.41 cnf(i_0_573, plain, (not_familiar(n6,n3)|familiar(n6,n3))). % 0.19/0.41 cnf(i_0_574, plain, (not_familiar(n6,n4)|familiar(n6,n4))). % 0.19/0.41 cnf(i_0_575, plain, (not_familiar(n6,n5)|familiar(n6,n5))). % 0.19/0.41 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.19/0.41 # Begin printing tableau % 0.19/0.41 # Found 3 steps % 0.19/0.41 cnf(i_0_888, negated_conjecture, (~not_familiar(n3,n4)|~not_familiar(n4,n6)|~not_familiar(n6,n3)), inference(start_rule)). % 0.19/0.41 cnf(i_0_1027, plain, (~not_familiar(n3,n4)), inferen# 24230 Satisfiable branch % 0.19/0.41 ce(extension_rule, [i_0_556])). % 0.19/0.41 cnf(i_0_1286, plain, (familiar(n3,n4)), inference(extension_rule, [i_0_672])). % 0.19/0.41 # End printing tableau % 0.19/0.41 # SZS output end % 0.19/0.41 # Branches closed with saturation will be marked with an "s" % 0.19/0.41 # 24232 Satisfiable branch % 0.19/0.41 # 24229 Satisfiable branch % 0.19/0.41 # 24233 Satisfiable branch % 0.19/0.41 # 24234 Satisfiable branch % 0.19/0.41 # 24235 Satisfiable branch % 0.19/0.41 # 24237 Satisfiable branch % 0.19/0.41 # Child (24236) has found a proof. % 0.19/0.41 % 0.19/0.41 # Proof search is over... % 0.19/0.41 # Freeing feature tree %------------------------------------------------------------------------------