%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ028-6 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 : Sun Sep 27 08:23:08 AM UTC 2026
% Result : Unsatisfiable 15.52s 2.42s
% Output : CNFRefutation 15.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 41
% Syntax : Number of formulae : 559 ( 81 unt; 0 def)
% Number of atoms : 1667 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1459 ( 351 ~;1108 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 71 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(familiar_or_not,axiom,
! [VAR_0,VAR_1] :
( ~ not_equal(VAR_0,VAR_1)
| ~ person(VAR_1)
| ~ person(VAR_0)
| not_familiar(VAR_0,VAR_1)
| familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',familiar_or_not) ).
cnf(c_1,plain,
( ~ not_equal(A,B)
| ~ person(B)
| ~ person(A)
| not_familiar(A,B)
| familiar(A,B) ),
inference(clausify,[status(thm)],[familiar_or_not]) ).
fof(not_equal_6_5,axiom,
not_equal(n6,n5),
file('theBenchmark.p',not_equal_6_5) ).
cnf(c_2,plain,
not_equal(n6,n5),
inference(clausify,[status(thm)],[not_equal_6_5]) ).
fof(not_equal_6_4,axiom,
not_equal(n6,n4),
file('theBenchmark.p',not_equal_6_4) ).
cnf(c_3,plain,
not_equal(n6,n4),
inference(clausify,[status(thm)],[not_equal_6_4]) ).
fof(not_equal_6_3,axiom,
not_equal(n6,n3),
file('theBenchmark.p',not_equal_6_3) ).
cnf(c_4,plain,
not_equal(n6,n3),
inference(clausify,[status(thm)],[not_equal_6_3]) ).
fof(not_equal_6_2,axiom,
not_equal(n6,n2),
file('theBenchmark.p',not_equal_6_2) ).
cnf(c_5,plain,
not_equal(n6,n2),
inference(clausify,[status(thm)],[not_equal_6_2]) ).
fof(not_equal_6_1,axiom,
not_equal(n6,n1),
file('theBenchmark.p',not_equal_6_1) ).
cnf(c_6,plain,
not_equal(n6,n1),
inference(clausify,[status(thm)],[not_equal_6_1]) ).
fof(not_equal_5_6,axiom,
not_equal(n5,n6),
file('theBenchmark.p',not_equal_5_6) ).
cnf(c_7,plain,
not_equal(n5,n6),
inference(clausify,[status(thm)],[not_equal_5_6]) ).
fof(not_equal_5_4,axiom,
not_equal(n5,n4),
file('theBenchmark.p',not_equal_5_4) ).
cnf(c_8,plain,
not_equal(n5,n4),
inference(clausify,[status(thm)],[not_equal_5_4]) ).
fof(not_equal_5_3,axiom,
not_equal(n5,n3),
file('theBenchmark.p',not_equal_5_3) ).
cnf(c_9,plain,
not_equal(n5,n3),
inference(clausify,[status(thm)],[not_equal_5_3]) ).
fof(not_equal_5_2,axiom,
not_equal(n5,n2),
file('theBenchmark.p',not_equal_5_2) ).
cnf(c_10,plain,
not_equal(n5,n2),
inference(clausify,[status(thm)],[not_equal_5_2]) ).
fof(not_equal_5_1,axiom,
not_equal(n5,n1),
file('theBenchmark.p',not_equal_5_1) ).
cnf(c_11,plain,
not_equal(n5,n1),
inference(clausify,[status(thm)],[not_equal_5_1]) ).
fof(not_equal_4_6,axiom,
not_equal(n4,n6),
file('theBenchmark.p',not_equal_4_6) ).
cnf(c_12,plain,
not_equal(n4,n6),
inference(clausify,[status(thm)],[not_equal_4_6]) ).
fof(not_equal_4_5,axiom,
not_equal(n4,n5),
file('theBenchmark.p',not_equal_4_5) ).
cnf(c_13,plain,
not_equal(n4,n5),
inference(clausify,[status(thm)],[not_equal_4_5]) ).
fof(not_equal_4_3,axiom,
not_equal(n4,n3),
file('theBenchmark.p',not_equal_4_3) ).
cnf(c_14,plain,
not_equal(n4,n3),
inference(clausify,[status(thm)],[not_equal_4_3]) ).
fof(not_equal_4_2,axiom,
not_equal(n4,n2),
file('theBenchmark.p',not_equal_4_2) ).
cnf(c_15,plain,
not_equal(n4,n2),
inference(clausify,[status(thm)],[not_equal_4_2]) ).
fof(not_equal_4_1,axiom,
not_equal(n4,n1),
file('theBenchmark.p',not_equal_4_1) ).
cnf(c_16,plain,
not_equal(n4,n1),
inference(clausify,[status(thm)],[not_equal_4_1]) ).
fof(not_equal_3_6,axiom,
not_equal(n3,n6),
file('theBenchmark.p',not_equal_3_6) ).
cnf(c_17,plain,
not_equal(n3,n6),
inference(clausify,[status(thm)],[not_equal_3_6]) ).
fof(not_equal_3_5,axiom,
not_equal(n3,n5),
file('theBenchmark.p',not_equal_3_5) ).
cnf(c_18,plain,
not_equal(n3,n5),
inference(clausify,[status(thm)],[not_equal_3_5]) ).
fof(not_equal_3_4,axiom,
not_equal(n3,n4),
file('theBenchmark.p',not_equal_3_4) ).
cnf(c_19,plain,
not_equal(n3,n4),
inference(clausify,[status(thm)],[not_equal_3_4]) ).
fof(not_equal_3_2,axiom,
not_equal(n3,n2),
file('theBenchmark.p',not_equal_3_2) ).
cnf(c_20,plain,
not_equal(n3,n2),
inference(clausify,[status(thm)],[not_equal_3_2]) ).
fof(not_equal_3_1,axiom,
not_equal(n3,n1),
file('theBenchmark.p',not_equal_3_1) ).
cnf(c_21,plain,
not_equal(n3,n1),
inference(clausify,[status(thm)],[not_equal_3_1]) ).
fof(not_equal_2_6,axiom,
not_equal(n2,n6),
file('theBenchmark.p',not_equal_2_6) ).
cnf(c_22,plain,
not_equal(n2,n6),
inference(clausify,[status(thm)],[not_equal_2_6]) ).
fof(not_equal_2_5,axiom,
not_equal(n2,n5),
file('theBenchmark.p',not_equal_2_5) ).
cnf(c_23,plain,
not_equal(n2,n5),
inference(clausify,[status(thm)],[not_equal_2_5]) ).
fof(not_equal_2_4,axiom,
not_equal(n2,n4),
file('theBenchmark.p',not_equal_2_4) ).
cnf(c_24,plain,
not_equal(n2,n4),
inference(clausify,[status(thm)],[not_equal_2_4]) ).
fof(not_equal_2_3,axiom,
not_equal(n2,n3),
file('theBenchmark.p',not_equal_2_3) ).
cnf(c_25,plain,
not_equal(n2,n3),
inference(clausify,[status(thm)],[not_equal_2_3]) ).
fof(not_equal_2_1,axiom,
not_equal(n2,n1),
file('theBenchmark.p',not_equal_2_1) ).
cnf(c_26,plain,
not_equal(n2,n1),
inference(clausify,[status(thm)],[not_equal_2_1]) ).
fof(not_equal_1_6,axiom,
not_equal(n1,n6),
file('theBenchmark.p',not_equal_1_6) ).
cnf(c_27,plain,
not_equal(n1,n6),
inference(clausify,[status(thm)],[not_equal_1_6]) ).
fof(not_equal_1_5,axiom,
not_equal(n1,n5),
file('theBenchmark.p',not_equal_1_5) ).
cnf(c_28,plain,
not_equal(n1,n5),
inference(clausify,[status(thm)],[not_equal_1_5]) ).
fof(not_equal_1_4,axiom,
not_equal(n1,n4),
file('theBenchmark.p',not_equal_1_4) ).
cnf(c_29,plain,
not_equal(n1,n4),
inference(clausify,[status(thm)],[not_equal_1_4]) ).
fof(not_equal_1_3,axiom,
not_equal(n1,n3),
file('theBenchmark.p',not_equal_1_3) ).
cnf(c_30,plain,
not_equal(n1,n3),
inference(clausify,[status(thm)],[not_equal_1_3]) ).
fof(not_equal_1_2,axiom,
not_equal(n1,n2),
file('theBenchmark.p',not_equal_1_2) ).
cnf(c_31,plain,
not_equal(n1,n2),
inference(clausify,[status(thm)],[not_equal_1_2]) ).
cnf(c_32,plain,
( ~ person(n2)
| ~ person(n1)
| not_familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_1,c_31]) ).
cnf(c_33,plain,
( ~ person(n3)
| ~ person(n1)
| not_familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_1,c_30]) ).
cnf(c_34,plain,
( ~ person(n4)
| ~ person(n1)
| not_familiar(n1,n4)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_1,c_29]) ).
cnf(c_35,plain,
( ~ person(n5)
| ~ person(n1)
| not_familiar(n1,n5)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_1,c_28]) ).
cnf(c_36,plain,
( ~ person(n6)
| ~ person(n1)
| not_familiar(n1,n6)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_1,c_27]) ).
cnf(c_37,plain,
( ~ person(n1)
| ~ person(n2)
| not_familiar(n2,n1)
| familiar(n2,n1) ),
inference(resolve,[status(thm)],[c_1,c_26]) ).
cnf(c_38,plain,
( ~ person(n3)
| ~ person(n2)
| not_familiar(n2,n3)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_1,c_25]) ).
cnf(c_39,plain,
( ~ person(n4)
| ~ person(n2)
| not_familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_1,c_24]) ).
cnf(c_40,plain,
( ~ person(n5)
| ~ person(n2)
| not_familiar(n2,n5)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_1,c_23]) ).
cnf(c_41,plain,
( ~ person(n6)
| ~ person(n2)
| not_familiar(n2,n6)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_1,c_22]) ).
cnf(c_42,plain,
( ~ person(n1)
| ~ person(n3)
| not_familiar(n3,n1)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_1,c_21]) ).
cnf(c_43,plain,
( ~ person(n2)
| ~ person(n3)
| not_familiar(n3,n2)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_1,c_20]) ).
cnf(c_44,plain,
( ~ person(n4)
| ~ person(n3)
| not_familiar(n3,n4)
| familiar(n3,n4) ),
inference(resolve,[status(thm)],[c_1,c_19]) ).
cnf(c_45,plain,
( ~ person(n5)
| ~ person(n3)
| not_familiar(n3,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_1,c_18]) ).
cnf(c_46,plain,
( ~ person(n6)
| ~ person(n3)
| not_familiar(n3,n6)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_1,c_17]) ).
cnf(c_47,plain,
( ~ person(n1)
| ~ person(n4)
| not_familiar(n4,n1)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_1,c_16]) ).
cnf(c_48,plain,
( ~ person(n2)
| ~ person(n4)
| not_familiar(n4,n2)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_1,c_15]) ).
cnf(c_49,plain,
( ~ person(n3)
| ~ person(n4)
| not_familiar(n4,n3)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_1,c_14]) ).
cnf(c_50,plain,
( ~ person(n5)
| ~ person(n4)
| not_familiar(n4,n5)
| familiar(n4,n5) ),
inference(resolve,[status(thm)],[c_1,c_13]) ).
cnf(c_51,plain,
( ~ person(n6)
| ~ person(n4)
| not_familiar(n4,n6)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_1,c_12]) ).
cnf(c_52,plain,
( ~ person(n1)
| ~ person(n5)
| not_familiar(n5,n1)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_1,c_11]) ).
cnf(c_53,plain,
( ~ person(n2)
| ~ person(n5)
| not_familiar(n5,n2)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_1,c_10]) ).
cnf(c_54,plain,
( ~ person(n3)
| ~ person(n5)
| not_familiar(n5,n3)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_1,c_9]) ).
cnf(c_55,plain,
( ~ person(n4)
| ~ person(n5)
| not_familiar(n5,n4)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_1,c_8]) ).
cnf(c_56,plain,
( ~ person(n6)
| ~ person(n5)
| not_familiar(n5,n6)
| familiar(n5,n6) ),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_57,plain,
( ~ person(n1)
| ~ person(n6)
| not_familiar(n6,n1)
| familiar(n6,n1) ),
inference(resolve,[status(thm)],[c_1,c_6]) ).
cnf(c_58,plain,
( ~ person(n2)
| ~ person(n6)
| not_familiar(n6,n2)
| familiar(n6,n2) ),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_59,plain,
( ~ person(n3)
| ~ person(n6)
| not_familiar(n6,n3)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_60,plain,
( ~ person(n4)
| ~ person(n6)
| not_familiar(n6,n4)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
cnf(c_61,plain,
( ~ person(n5)
| ~ person(n6)
| not_familiar(n6,n5)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(three_not_familiar,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ not_familiar(VAR_2,VAR_0)
| ~ not_familiar(VAR_1,VAR_2)
| ~ not_familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',three_not_familiar) ).
cnf(c_62,plain,
( ~ not_familiar(C,A)
| ~ not_familiar(B,C)
| ~ not_familiar(A,B) ),
inference(clausify,[status(thm)],[three_not_familiar]) ).
fof(three_familiar,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ familiar(VAR_2,VAR_0)
| ~ familiar(VAR_1,VAR_2)
| ~ familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',three_familiar) ).
cnf(c_63,plain,
( ~ familiar(C,A)
| ~ familiar(B,C)
| ~ familiar(A,B) ),
inference(clausify,[status(thm)],[three_familiar]) ).
fof(symmetry_of_not_familiar,axiom,
! [VAR_0,VAR_1] :
( not_familiar(VAR_1,VAR_0)
| ~ not_familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',symmetry_of_not_familiar) ).
cnf(c_64,plain,
( not_familiar(B,A)
| ~ not_familiar(A,B) ),
inference(clausify,[status(thm)],[symmetry_of_not_familiar]) ).
fof(symmetry_of_familiar,axiom,
! [VAR_0,VAR_1] :
( familiar(VAR_1,VAR_0)
| ~ familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',symmetry_of_familiar) ).
cnf(c_65,plain,
( familiar(B,A)
| ~ familiar(A,B) ),
inference(clausify,[status(thm)],[symmetry_of_familiar]) ).
fof(person_6,axiom,
person(n6),
file('theBenchmark.p',person_6) ).
cnf(c_66,plain,
person(n6),
inference(clausify,[status(thm)],[person_6]) ).
fof(person_5,axiom,
person(n5),
file('theBenchmark.p',person_5) ).
cnf(c_67,plain,
person(n5),
inference(clausify,[status(thm)],[person_5]) ).
fof(person_4,axiom,
person(n4),
file('theBenchmark.p',person_4) ).
cnf(c_68,plain,
person(n4),
inference(clausify,[status(thm)],[person_4]) ).
fof(person_3,axiom,
person(n3),
file('theBenchmark.p',person_3) ).
cnf(c_69,plain,
person(n3),
inference(clausify,[status(thm)],[person_3]) ).
fof(person_2,axiom,
person(n2),
file('theBenchmark.p',person_2) ).
cnf(c_70,plain,
person(n2),
inference(clausify,[status(thm)],[person_2]) ).
fof(person_1,axiom,
person(n1),
file('theBenchmark.p',person_1) ).
cnf(c_71,plain,
person(n1),
inference(clausify,[status(thm)],[person_1]) ).
cnf(c_6966,plain,
( ~ person(n5)
| not_familiar(n6,n5)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_66,c_61]) ).
cnf(c_74,plain,
( not_familiar(n6,n5)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_67,c_6966]) ).
cnf(c_6967,plain,
( ~ person(n4)
| not_familiar(n6,n4)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_66,c_60]) ).
cnf(c_75,plain,
( not_familiar(n6,n4)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_68,c_6967]) ).
cnf(c_6968,plain,
( ~ person(n3)
| not_familiar(n6,n3)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_66,c_59]) ).
cnf(c_76,plain,
( not_familiar(n6,n3)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_69,c_6968]) ).
cnf(c_6969,plain,
( ~ person(n2)
| not_familiar(n6,n2)
| familiar(n6,n2) ),
inference(resolve,[status(thm)],[c_66,c_58]) ).
cnf(c_77,plain,
( not_familiar(n6,n2)
| familiar(n6,n2) ),
inference(resolve,[status(thm)],[c_70,c_6969]) ).
cnf(c_6970,plain,
( ~ person(n1)
| not_familiar(n6,n1)
| familiar(n6,n1) ),
inference(resolve,[status(thm)],[c_66,c_57]) ).
cnf(c_78,plain,
( not_familiar(n6,n1)
| familiar(n6,n1) ),
inference(resolve,[status(thm)],[c_71,c_6970]) ).
cnf(c_6971,plain,
( ~ person(n6)
| not_familiar(n5,n6)
| familiar(n5,n6) ),
inference(resolve,[status(thm)],[c_67,c_56]) ).
cnf(c_79,plain,
( not_familiar(n5,n6)
| familiar(n5,n6) ),
inference(resolve,[status(thm)],[c_66,c_6971]) ).
cnf(c_6972,plain,
( ~ person(n6)
| not_familiar(n4,n6)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_68,c_51]) ).
cnf(c_80,plain,
( not_familiar(n4,n6)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_66,c_6972]) ).
cnf(c_6973,plain,
( ~ person(n6)
| not_familiar(n3,n6)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_69,c_46]) ).
cnf(c_81,plain,
( not_familiar(n3,n6)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_66,c_6973]) ).
cnf(c_6974,plain,
( ~ person(n6)
| not_familiar(n2,n6)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_70,c_41]) ).
cnf(c_82,plain,
( not_familiar(n2,n6)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_66,c_6974]) ).
cnf(c_6975,plain,
( ~ person(n6)
| not_familiar(n1,n6)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_71,c_36]) ).
cnf(c_83,plain,
( not_familiar(n1,n6)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_66,c_6975]) ).
cnf(c_6976,plain,
( ~ person(n4)
| not_familiar(n5,n4)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_67,c_55]) ).
cnf(c_84,plain,
( not_familiar(n5,n4)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_68,c_6976]) ).
cnf(c_6977,plain,
( ~ person(n3)
| not_familiar(n5,n3)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_67,c_54]) ).
cnf(c_85,plain,
( not_familiar(n5,n3)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_69,c_6977]) ).
cnf(c_6978,plain,
( ~ person(n2)
| not_familiar(n5,n2)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_67,c_53]) ).
cnf(c_86,plain,
( not_familiar(n5,n2)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_70,c_6978]) ).
cnf(c_6979,plain,
( ~ person(n1)
| not_familiar(n5,n1)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_67,c_52]) ).
cnf(c_87,plain,
( not_familiar(n5,n1)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_71,c_6979]) ).
cnf(c_6980,plain,
( ~ person(n5)
| not_familiar(n4,n5)
| familiar(n4,n5) ),
inference(resolve,[status(thm)],[c_68,c_50]) ).
cnf(c_88,plain,
( not_familiar(n4,n5)
| familiar(n4,n5) ),
inference(resolve,[status(thm)],[c_67,c_6980]) ).
cnf(c_6981,plain,
( ~ person(n5)
| not_familiar(n3,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_69,c_45]) ).
cnf(c_89,plain,
( not_familiar(n3,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_67,c_6981]) ).
cnf(c_6982,plain,
( ~ person(n5)
| not_familiar(n2,n5)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_70,c_40]) ).
cnf(c_90,plain,
( not_familiar(n2,n5)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_67,c_6982]) ).
cnf(c_6983,plain,
( ~ person(n5)
| not_familiar(n1,n5)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_71,c_35]) ).
cnf(c_91,plain,
( not_familiar(n1,n5)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_67,c_6983]) ).
cnf(c_6984,plain,
( ~ person(n3)
| not_familiar(n4,n3)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_68,c_49]) ).
cnf(c_92,plain,
( not_familiar(n4,n3)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_69,c_6984]) ).
cnf(c_6985,plain,
( ~ person(n2)
| not_familiar(n4,n2)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_68,c_48]) ).
cnf(c_93,plain,
( not_familiar(n4,n2)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_70,c_6985]) ).
cnf(c_6986,plain,
( ~ person(n1)
| not_familiar(n4,n1)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_68,c_47]) ).
cnf(c_94,plain,
( not_familiar(n4,n1)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_71,c_6986]) ).
cnf(c_6987,plain,
( ~ person(n4)
| not_familiar(n3,n4)
| familiar(n3,n4) ),
inference(resolve,[status(thm)],[c_69,c_44]) ).
cnf(c_95,plain,
( not_familiar(n3,n4)
| familiar(n3,n4) ),
inference(resolve,[status(thm)],[c_68,c_6987]) ).
cnf(c_6988,plain,
( ~ person(n4)
| not_familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_70,c_39]) ).
cnf(c_96,plain,
( not_familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_68,c_6988]) ).
cnf(c_6989,plain,
( ~ person(n4)
| not_familiar(n1,n4)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_71,c_34]) ).
cnf(c_97,plain,
( not_familiar(n1,n4)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_68,c_6989]) ).
cnf(c_6990,plain,
( ~ person(n2)
| not_familiar(n3,n2)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_69,c_43]) ).
cnf(c_98,plain,
( not_familiar(n3,n2)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_70,c_6990]) ).
cnf(c_6991,plain,
( ~ person(n1)
| not_familiar(n3,n1)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_69,c_42]) ).
cnf(c_99,plain,
( not_familiar(n3,n1)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_71,c_6991]) ).
cnf(c_6992,plain,
( ~ person(n3)
| not_familiar(n2,n3)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_70,c_38]) ).
cnf(c_100,plain,
( not_familiar(n2,n3)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_69,c_6992]) ).
cnf(c_6993,plain,
( ~ person(n3)
| not_familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_71,c_33]) ).
cnf(c_101,plain,
( not_familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_69,c_6993]) ).
cnf(c_6994,plain,
( ~ person(n1)
| not_familiar(n2,n1)
| familiar(n2,n1) ),
inference(resolve,[status(thm)],[c_70,c_37]) ).
cnf(c_102,plain,
( not_familiar(n2,n1)
| familiar(n2,n1) ),
inference(resolve,[status(thm)],[c_71,c_6994]) ).
cnf(c_6995,plain,
( ~ person(n2)
| not_familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_71,c_32]) ).
cnf(c_103,plain,
( not_familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_70,c_6995]) ).
cnf(c_105,plain,
( ~ not_familiar(A,n6)
| ~ not_familiar(n5,A)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_74,c_62]) ).
cnf(c_106,plain,
( not_familiar(n4,n6)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_75,c_64]) ).
cnf(c_107,plain,
( ~ not_familiar(A,n6)
| ~ not_familiar(n4,A)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_75,c_62]) ).
cnf(c_108,plain,
( not_familiar(n3,n6)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_76,c_64]) ).
cnf(c_109,plain,
( ~ not_familiar(A,n6)
| ~ not_familiar(n3,A)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_76,c_62]) ).
cnf(c_110,plain,
( not_familiar(n2,n6)
| familiar(n6,n2) ),
inference(resolve,[status(thm)],[c_77,c_64]) ).
cnf(c_112,plain,
( not_familiar(n1,n6)
| familiar(n6,n1) ),
inference(resolve,[status(thm)],[c_78,c_64]) ).
cnf(c_117,plain,
( ~ not_familiar(A,n4)
| ~ not_familiar(n6,A)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_80,c_62]) ).
cnf(c_119,plain,
( ~ not_familiar(A,n3)
| ~ not_familiar(n6,A)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_81,c_62]) ).
cnf(c_120,plain,
( not_familiar(n6,n2)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_82,c_64]) ).
cnf(c_121,plain,
( ~ not_familiar(A,n2)
| ~ not_familiar(n6,A)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_82,c_62]) ).
cnf(c_122,plain,
( not_familiar(n6,n1)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_83,c_64]) ).
cnf(c_125,plain,
( ~ not_familiar(A,n5)
| ~ not_familiar(n4,A)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_84,c_62]) ).
cnf(c_126,plain,
( not_familiar(n3,n5)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_85,c_64]) ).
cnf(c_127,plain,
( ~ not_familiar(A,n5)
| ~ not_familiar(n3,A)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_85,c_62]) ).
cnf(c_128,plain,
( not_familiar(n2,n5)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_86,c_64]) ).
cnf(c_129,plain,
( ~ not_familiar(A,n5)
| ~ not_familiar(n2,A)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_86,c_62]) ).
cnf(c_130,plain,
( not_familiar(n1,n5)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_87,c_64]) ).
cnf(c_132,plain,
( not_familiar(n5,n4)
| familiar(n4,n5) ),
inference(resolve,[status(thm)],[c_88,c_64]) ).
cnf(c_135,plain,
( ~ not_familiar(A,n3)
| ~ not_familiar(n5,A)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_89,c_62]) ).
cnf(c_136,plain,
( not_familiar(n5,n2)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_90,c_64]) ).
cnf(c_137,plain,
( ~ not_familiar(A,n2)
| ~ not_familiar(n5,A)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_90,c_62]) ).
cnf(c_138,plain,
( not_familiar(n5,n1)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_91,c_64]) ).
cnf(c_141,plain,
( ~ not_familiar(A,n4)
| ~ not_familiar(n3,A)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_92,c_62]) ).
cnf(c_142,plain,
( not_familiar(n2,n4)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_93,c_64]) ).
cnf(c_143,plain,
( ~ not_familiar(A,n4)
| ~ not_familiar(n2,A)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_93,c_62]) ).
cnf(c_144,plain,
( not_familiar(n1,n4)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_94,c_64]) ).
cnf(c_146,plain,
( not_familiar(n4,n3)
| familiar(n3,n4) ),
inference(resolve,[status(thm)],[c_95,c_64]) ).
cnf(c_148,plain,
( not_familiar(n4,n2)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_96,c_64]) ).
cnf(c_149,plain,
( ~ not_familiar(A,n2)
| ~ not_familiar(n4,A)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_96,c_62]) ).
cnf(c_150,plain,
( not_familiar(n4,n1)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_97,c_64]) ).
cnf(c_152,plain,
( not_familiar(n2,n3)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_98,c_64]) ).
cnf(c_153,plain,
( ~ not_familiar(A,n3)
| ~ not_familiar(n2,A)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_98,c_62]) ).
cnf(c_154,plain,
( not_familiar(n1,n3)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_99,c_64]) ).
cnf(c_156,plain,
( not_familiar(n3,n2)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_100,c_64]) ).
cnf(c_158,plain,
( not_familiar(n3,n1)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_101,c_64]) ).
cnf(c_160,plain,
( not_familiar(n1,n2)
| familiar(n2,n1) ),
inference(resolve,[status(thm)],[c_102,c_64]) ).
cnf(c_162,plain,
( not_familiar(n2,n1)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_103,c_64]) ).
cnf(c_165,plain,
( familiar(n5,n1)
| ~ not_familiar(n1,n6)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_105,c_87]) ).
cnf(c_166,plain,
( familiar(n5,n2)
| ~ not_familiar(n2,n6)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_105,c_86]) ).
cnf(c_173,plain,
( ~ not_familiar(n5,n4)
| familiar(n6,n5)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_106,c_105]) ).
cnf(c_184,plain,
( familiar(n4,n1)
| ~ not_familiar(n1,n6)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_107,c_94]) ).
cnf(c_188,plain,
( familiar(n6,n1)
| ~ not_familiar(n4,n1)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_107,c_112]) ).
cnf(c_189,plain,
( familiar(n6,n2)
| ~ not_familiar(n4,n2)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_107,c_110]) ).
cnf(c_190,plain,
( familiar(n6,n3)
| ~ not_familiar(n4,n3)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_107,c_108]) ).
cnf(c_196,plain,
( familiar(n3,n1)
| ~ not_familiar(n1,n6)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_109,c_99]) ).
cnf(c_200,plain,
( familiar(n6,n1)
| ~ not_familiar(n3,n1)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_109,c_112]) ).
cnf(c_201,plain,
( familiar(n6,n2)
| ~ not_familiar(n3,n2)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_109,c_110]) ).
cnf(c_207,plain,
( familiar(n5,n6)
| ~ not_familiar(n3,n5)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_109,c_79]) ).
cnf(c_254,plain,
( familiar(n1,n6)
| ~ not_familiar(n1,n4)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_117,c_122]) ).
cnf(c_255,plain,
( familiar(n2,n6)
| ~ not_familiar(n2,n4)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_117,c_120]) ).
cnf(c_277,plain,
( familiar(n1,n6)
| ~ not_familiar(n1,n3)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_119,c_122]) ).
cnf(c_278,plain,
( familiar(n2,n6)
| ~ not_familiar(n2,n3)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_119,c_120]) ).
cnf(c_286,plain,
( familiar(n1,n6)
| ~ not_familiar(n1,n2)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_121,c_122]) ).
cnf(c_322,plain,
( familiar(n1,n4)
| ~ not_familiar(n1,n5)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_125,c_150]) ).
cnf(c_323,plain,
( familiar(n2,n4)
| ~ not_familiar(n2,n5)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_125,c_148]) ).
cnf(c_326,plain,
( familiar(n4,n1)
| ~ not_familiar(n1,n5)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_125,c_94]) ).
cnf(c_327,plain,
( familiar(n4,n2)
| ~ not_familiar(n2,n5)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_125,c_93]) ).
cnf(c_328,plain,
( familiar(n4,n3)
| ~ not_familiar(n3,n5)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_125,c_92]) ).
cnf(c_338,plain,
( familiar(n3,n1)
| ~ not_familiar(n1,n5)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_127,c_99]) ).
cnf(c_341,plain,
( familiar(n5,n1)
| ~ not_familiar(n3,n1)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_127,c_130]) ).
cnf(c_342,plain,
( familiar(n5,n2)
| ~ not_familiar(n3,n2)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_127,c_128]) ).
cnf(c_354,plain,
( familiar(n5,n1)
| ~ not_familiar(n2,n1)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_129,c_130]) ).
cnf(c_401,plain,
( familiar(n1,n5)
| ~ not_familiar(n1,n3)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_135,c_138]) ).
cnf(c_402,plain,
( familiar(n2,n5)
| ~ not_familiar(n2,n3)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_135,c_136]) ).
cnf(c_412,plain,
( familiar(n1,n5)
| ~ not_familiar(n1,n2)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_137,c_138]) ).
cnf(c_434,plain,
( familiar(n1,n3)
| ~ not_familiar(n1,n4)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_141,c_158]) ).
cnf(c_435,plain,
( familiar(n2,n3)
| ~ not_familiar(n2,n4)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_141,c_156]) ).
cnf(c_438,plain,
( familiar(n3,n1)
| ~ not_familiar(n1,n4)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_141,c_99]) ).
cnf(c_439,plain,
( familiar(n3,n2)
| ~ not_familiar(n2,n4)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_141,c_98]) ).
cnf(c_446,plain,
( familiar(n1,n2)
| ~ not_familiar(n1,n4)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_143,c_162]) ).
cnf(c_450,plain,
( familiar(n2,n1)
| ~ not_familiar(n1,n4)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_143,c_102]) ).
cnf(c_480,plain,
( familiar(n1,n4)
| ~ not_familiar(n1,n2)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_149,c_150]) ).
cnf(c_500,plain,
( familiar(n1,n2)
| ~ not_familiar(n1,n3)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_153,c_162]) ).
cnf(c_504,plain,
( familiar(n2,n1)
| ~ not_familiar(n1,n3)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_153,c_102]) ).
cnf(c_563,plain,
( familiar(n1,n6)
| familiar(n5,n1)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_165,c_83]) ).
cnf(c_565,plain,
( familiar(n2,n6)
| familiar(n5,n2)
| familiar(n6,n5) ),
inference(resolve,[status(thm)],[c_166,c_82]) ).
cnf(c_574,plain,
( familiar(n4,n5)
| familiar(n6,n5)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_173,c_132]) ).
cnf(c_623,plain,
( familiar(n1,n6)
| familiar(n4,n1)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_184,c_83]) ).
cnf(c_629,plain,
( familiar(n1,n4)
| familiar(n6,n1)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_188,c_150]) ).
cnf(c_630,plain,
( familiar(n2,n4)
| familiar(n6,n2)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_189,c_148]) ).
cnf(c_631,plain,
( familiar(n3,n4)
| familiar(n6,n3)
| familiar(n6,n4) ),
inference(resolve,[status(thm)],[c_190,c_146]) ).
cnf(c_637,plain,
( familiar(n1,n6)
| familiar(n3,n1)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_196,c_83]) ).
cnf(c_642,plain,
( familiar(n1,n3)
| familiar(n6,n1)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_200,c_158]) ).
cnf(c_643,plain,
( familiar(n2,n3)
| familiar(n6,n2)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_201,c_156]) ).
cnf(c_647,plain,
( familiar(n5,n3)
| familiar(n5,n6)
| familiar(n6,n3) ),
inference(resolve,[status(thm)],[c_207,c_126]) ).
cnf(c_706,plain,
( familiar(n4,n1)
| familiar(n1,n6)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_254,c_144]) ).
cnf(c_708,plain,
( familiar(n4,n2)
| familiar(n2,n6)
| familiar(n4,n6) ),
inference(resolve,[status(thm)],[c_255,c_142]) ).
cnf(c_733,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_277,c_101]) ).
cnf(c_735,plain,
( familiar(n2,n3)
| familiar(n2,n6)
| familiar(n3,n6) ),
inference(resolve,[status(thm)],[c_278,c_100]) ).
cnf(c_736,plain,
( familiar(n2,n1)
| familiar(n1,n6)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_286,c_160]) ).
cnf(c_737,plain,
( familiar(n1,n2)
| familiar(n1,n6)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_286,c_103]) ).
cnf(c_753,plain,
( familiar(n1,n5)
| familiar(n1,n4)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_322,c_91]) ).
cnf(c_755,plain,
( familiar(n2,n5)
| familiar(n2,n4)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_323,c_90]) ).
cnf(c_758,plain,
( familiar(n5,n1)
| familiar(n4,n1)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_326,c_130]) ).
cnf(c_759,plain,
( familiar(n1,n5)
| familiar(n4,n1)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_326,c_91]) ).
cnf(c_760,plain,
( familiar(n5,n2)
| familiar(n4,n2)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_327,c_128]) ).
cnf(c_761,plain,
( familiar(n2,n5)
| familiar(n4,n2)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_327,c_90]) ).
cnf(c_762,plain,
( familiar(n5,n3)
| familiar(n4,n3)
| familiar(n5,n4) ),
inference(resolve,[status(thm)],[c_328,c_126]) ).
cnf(c_766,plain,
( familiar(n1,n5)
| familiar(n3,n1)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_338,c_91]) ).
cnf(c_770,plain,
( familiar(n1,n3)
| familiar(n5,n1)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_341,c_158]) ).
cnf(c_771,plain,
( familiar(n2,n3)
| familiar(n5,n2)
| familiar(n5,n3) ),
inference(resolve,[status(thm)],[c_342,c_156]) ).
cnf(c_780,plain,
( familiar(n1,n2)
| familiar(n5,n1)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_354,c_162]) ).
cnf(c_796,plain,
( familiar(n3,n1)
| familiar(n1,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_401,c_154]) ).
cnf(c_797,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_401,c_101]) ).
cnf(c_798,plain,
( familiar(n3,n2)
| familiar(n2,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_402,c_152]) ).
cnf(c_799,plain,
( familiar(n2,n3)
| familiar(n2,n5)
| familiar(n3,n5) ),
inference(resolve,[status(thm)],[c_402,c_100]) ).
cnf(c_800,plain,
( familiar(n2,n1)
| familiar(n1,n5)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_412,c_160]) ).
cnf(c_801,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_412,c_103]) ).
cnf(c_802,plain,
( familiar(n4,n1)
| familiar(n1,n3)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_434,c_144]) ).
cnf(c_803,plain,
( familiar(n1,n4)
| familiar(n1,n3)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_434,c_97]) ).
cnf(c_804,plain,
( familiar(n4,n2)
| familiar(n2,n3)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_435,c_142]) ).
cnf(c_807,plain,
( familiar(n1,n4)
| familiar(n3,n1)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_438,c_97]) ).
cnf(c_809,plain,
( familiar(n2,n4)
| familiar(n3,n2)
| familiar(n4,n3) ),
inference(resolve,[status(thm)],[c_439,c_96]) ).
cnf(c_810,plain,
( familiar(n4,n1)
| familiar(n1,n2)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_446,c_144]) ).
cnf(c_813,plain,
( familiar(n4,n1)
| familiar(n2,n1)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_450,c_144]) ).
cnf(c_814,plain,
( familiar(n1,n4)
| familiar(n2,n1)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_450,c_97]) ).
cnf(c_825,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_480,c_103]) ).
cnf(c_826,plain,
( familiar(n3,n1)
| familiar(n1,n2)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_500,c_154]) ).
cnf(c_828,plain,
( familiar(n3,n1)
| familiar(n2,n1)
| familiar(n3,n2) ),
inference(resolve,[status(thm)],[c_504,c_154]) ).
cnf(c_835,plain,
( ~ familiar(A,n6)
| ~ familiar(n5,A)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_563,c_63]) ).
cnf(c_837,plain,
( ~ familiar(A,n6)
| ~ familiar(n5,A)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_565,c_63]) ).
cnf(c_851,plain,
( ~ familiar(A,n6)
| ~ familiar(n4,A)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_623,c_63]) ).
cnf(c_865,plain,
( ~ familiar(A,n6)
| ~ familiar(n3,A)
| familiar(n1,n6)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_637,c_63]) ).
cnf(c_915,plain,
( ~ familiar(A,n5)
| ~ familiar(n4,A)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_753,c_63]) ).
cnf(c_917,plain,
( ~ familiar(A,n5)
| ~ familiar(n4,A)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_755,c_63]) ).
cnf(c_921,plain,
( ~ familiar(A,n5)
| ~ familiar(n4,A)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_759,c_63]) ).
cnf(c_923,plain,
( ~ familiar(A,n5)
| ~ familiar(n4,A)
| familiar(n2,n5)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_761,c_63]) ).
cnf(c_928,plain,
( ~ familiar(A,n5)
| ~ familiar(n3,A)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_766,c_63]) ).
cnf(c_963,plain,
( ~ familiar(A,n4)
| ~ familiar(n3,A)
| familiar(n1,n4)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_803,c_63]) ).
cnf(c_964,plain,
( ~ familiar(A,n4)
| ~ familiar(n3,A)
| familiar(n4,n2)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_804,c_63]) ).
cnf(c_967,plain,
( ~ familiar(A,n4)
| ~ familiar(n3,A)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_807,c_63]) ).
cnf(c_6996,plain,
( familiar(n1,n2)
| familiar(n5,n1)
| ~ familiar(n2,n6)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_835,c_780]) ).
cnf(c_1037,plain,
( familiar(n1,n2)
| ~ familiar(n2,n6)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_6996]) ).
cnf(c_6997,plain,
( familiar(n1,n3)
| familiar(n5,n1)
| ~ familiar(n3,n6)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_835,c_770]) ).
cnf(c_1047,plain,
( familiar(n1,n3)
| ~ familiar(n3,n6)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_6997]) ).
cnf(c_6998,plain,
( familiar(n5,n1)
| familiar(n4,n1)
| ~ familiar(n4,n6)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_835,c_758]) ).
cnf(c_1059,plain,
( familiar(n4,n1)
| ~ familiar(n4,n6)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_6998]) ).
cnf(c_6999,plain,
( familiar(n2,n3)
| familiar(n5,n2)
| ~ familiar(n3,n6)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_837,c_771]) ).
cnf(c_1124,plain,
( familiar(n2,n3)
| ~ familiar(n3,n6)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(copy,[status(thm)],[c_6999]) ).
cnf(c_7000,plain,
( familiar(n5,n2)
| familiar(n4,n2)
| ~ familiar(n4,n6)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_837,c_760]) ).
cnf(c_1135,plain,
( familiar(n4,n2)
| ~ familiar(n4,n6)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(copy,[status(thm)],[c_7000]) ).
cnf(c_7001,plain,
( familiar(n4,n1)
| familiar(n2,n1)
| ~ familiar(n2,n6)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_851,c_813]) ).
cnf(c_1568,plain,
( familiar(n2,n1)
| ~ familiar(n2,n6)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7001]) ).
cnf(c_7002,plain,
( familiar(n4,n1)
| familiar(n1,n3)
| ~ familiar(n3,n6)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_851,c_802]) ).
cnf(c_1579,plain,
( familiar(n1,n3)
| ~ familiar(n3,n6)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7002]) ).
cnf(c_7003,plain,
( familiar(n3,n1)
| familiar(n1,n2)
| ~ familiar(n2,n6)
| familiar(n1,n6)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_865,c_826]) ).
cnf(c_1927,plain,
( familiar(n1,n2)
| ~ familiar(n2,n6)
| familiar(n1,n6)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7003]) ).
cnf(c_7004,plain,
( familiar(n1,n4)
| familiar(n2,n1)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_915,c_814]) ).
cnf(c_2605,plain,
( familiar(n2,n1)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7004]) ).
cnf(c_7005,plain,
( familiar(n1,n4)
| familiar(n3,n1)
| ~ familiar(n3,n5)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_915,c_807]) ).
cnf(c_2610,plain,
( familiar(n3,n1)
| ~ familiar(n3,n5)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7005]) ).
cnf(c_7006,plain,
( familiar(n2,n4)
| familiar(n3,n2)
| ~ familiar(n3,n5)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_917,c_809]) ).
cnf(c_2638,plain,
( familiar(n3,n2)
| ~ familiar(n3,n5)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(copy,[status(thm)],[c_7006]) ).
cnf(c_7007,plain,
( familiar(n4,n1)
| familiar(n1,n2)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_921,c_810]) ).
cnf(c_2691,plain,
( familiar(n1,n2)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7007]) ).
cnf(c_7008,plain,
( familiar(n4,n1)
| familiar(n1,n3)
| ~ familiar(n3,n5)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_921,c_802]) ).
cnf(c_2697,plain,
( familiar(n1,n3)
| ~ familiar(n3,n5)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7008]) ).
cnf(c_7009,plain,
( familiar(n4,n2)
| familiar(n2,n3)
| ~ familiar(n3,n5)
| familiar(n2,n5)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_923,c_804]) ).
cnf(c_2721,plain,
( familiar(n2,n3)
| ~ familiar(n3,n5)
| familiar(n2,n5)
| familiar(n4,n2) ),
inference(copy,[status(thm)],[c_7009]) ).
cnf(c_7010,plain,
( familiar(n3,n1)
| familiar(n2,n1)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_928,c_828]) ).
cnf(c_2767,plain,
( familiar(n2,n1)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7010]) ).
cnf(c_7011,plain,
( familiar(n3,n1)
| familiar(n1,n2)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_928,c_826]) ).
cnf(c_2769,plain,
( familiar(n1,n2)
| ~ familiar(n2,n5)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7011]) ).
cnf(c_7012,plain,
( familiar(n3,n1)
| familiar(n1,n2)
| ~ familiar(n2,n4)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_967,c_826]) ).
cnf(c_3009,plain,
( familiar(n1,n2)
| ~ familiar(n2,n4)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7012]) ).
cnf(c_7013,plain,
( familiar(n1,n2)
| familiar(n1,n6)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_1037,c_737]) ).
cnf(c_7014,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_7013]) ).
cnf(c_3057,plain,
( familiar(n1,n2)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_7014]) ).
cnf(c_3060,plain,
( familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3057,c_65]) ).
cnf(c_3085,plain,
( ~ familiar(A,n1)
| ~ familiar(n6,A)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_3060,c_63]) ).
cnf(c_7015,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_1047,c_733]) ).
cnf(c_7016,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_7015]) ).
cnf(c_3101,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_7016]) ).
cnf(c_3104,plain,
( familiar(n1,n5)
| familiar(n1,n3)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3101,c_65]) ).
cnf(c_3125,plain,
( ~ familiar(A,n1)
| ~ familiar(n6,A)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_3104,c_63]) ).
cnf(c_7017,plain,
( familiar(n4,n1)
| familiar(n1,n6)
| familiar(n4,n1)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(resolve,[status(thm)],[c_1059,c_706]) ).
cnf(c_7018,plain,
( familiar(n4,n1)
| familiar(n4,n1)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_7017]) ).
cnf(c_3150,plain,
( familiar(n4,n1)
| familiar(n1,n6)
| familiar(n5,n1) ),
inference(copy,[status(thm)],[c_7018]) ).
cnf(c_3153,plain,
( familiar(n1,n5)
| familiar(n4,n1)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3150,c_65]) ).
cnf(c_3157,plain,
( familiar(n1,n4)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3153,c_65]) ).
cnf(c_3175,plain,
( ~ familiar(A,n1)
| ~ familiar(n6,A)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_3157,c_63]) ).
cnf(c_7019,plain,
( familiar(n2,n3)
| familiar(n2,n6)
| familiar(n2,n3)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_1124,c_735]) ).
cnf(c_7020,plain,
( familiar(n2,n3)
| familiar(n2,n3)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(copy,[status(thm)],[c_7019]) ).
cnf(c_3228,plain,
( familiar(n2,n3)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(copy,[status(thm)],[c_7020]) ).
cnf(c_3233,plain,
( familiar(n2,n5)
| familiar(n2,n3)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_3228,c_65]) ).
cnf(c_3234,plain,
( ~ familiar(A,n5)
| ~ familiar(n2,A)
| familiar(n2,n3)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_3228,c_63]) ).
cnf(c_3257,plain,
( ~ familiar(A,n2)
| ~ familiar(n6,A)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_3233,c_63]) ).
cnf(c_7021,plain,
( familiar(n4,n2)
| familiar(n2,n6)
| familiar(n4,n2)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(resolve,[status(thm)],[c_1135,c_708]) ).
cnf(c_7022,plain,
( familiar(n4,n2)
| familiar(n4,n2)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(copy,[status(thm)],[c_7021]) ).
cnf(c_3286,plain,
( familiar(n4,n2)
| familiar(n2,n6)
| familiar(n5,n2) ),
inference(copy,[status(thm)],[c_7022]) ).
cnf(c_3291,plain,
( familiar(n2,n5)
| familiar(n4,n2)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_3286,c_65]) ).
cnf(c_3297,plain,
( familiar(n2,n4)
| familiar(n2,n5)
| familiar(n2,n6) ),
inference(resolve,[status(thm)],[c_3291,c_65]) ).
cnf(c_3318,plain,
( ~ familiar(A,n2)
| ~ familiar(n6,A)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_3297,c_63]) ).
cnf(c_7023,plain,
( familiar(n2,n1)
| familiar(n1,n6)
| familiar(n2,n1)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_1568,c_736]) ).
cnf(c_7024,plain,
( familiar(n2,n1)
| familiar(n2,n1)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7023]) ).
cnf(c_3488,plain,
( familiar(n2,n1)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7024]) ).
cnf(c_3495,plain,
( familiar(n1,n4)
| familiar(n2,n1)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3488,c_65]) ).
cnf(c_3501,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3495,c_65]) ).
cnf(c_3538,plain,
( familiar(n6,n1)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_3501,c_65]) ).
cnf(c_3539,plain,
( ~ familiar(A,n1)
| ~ familiar(n6,A)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_3501,c_63]) ).
cnf(c_3542,plain,
( ~ familiar(A,n6)
| ~ familiar(n1,A)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_3538,c_63]) ).
cnf(c_7025,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_1579,c_733]) ).
cnf(c_7026,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7025]) ).
cnf(c_3611,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7026]) ).
cnf(c_3618,plain,
( ~ familiar(A,n4)
| ~ familiar(n1,A)
| familiar(n1,n3)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3611,c_63]) ).
cnf(c_7027,plain,
( familiar(n1,n2)
| familiar(n1,n6)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_1927,c_737]) ).
cnf(c_7028,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7027]) ).
cnf(c_3842,plain,
( familiar(n1,n2)
| familiar(n1,n6)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7028]) ).
cnf(c_3851,plain,
( ~ familiar(A,n3)
| ~ familiar(n1,A)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolve,[status(thm)],[c_3842,c_63]) ).
cnf(c_7029,plain,
( familiar(n2,n1)
| familiar(n1,n5)
| familiar(n2,n1)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_2605,c_800]) ).
cnf(c_7030,plain,
( familiar(n2,n1)
| familiar(n2,n1)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7029]) ).
cnf(c_4007,plain,
( familiar(n2,n1)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7030]) ).
cnf(c_4014,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_4007,c_65]) ).
cnf(c_4038,plain,
( ~ familiar(A,n1)
| ~ familiar(n5,A)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_4014,c_63]) ).
cnf(c_7031,plain,
( familiar(n3,n1)
| familiar(n1,n5)
| familiar(n3,n1)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_2610,c_796]) ).
cnf(c_7032,plain,
( familiar(n3,n1)
| familiar(n3,n1)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7031]) ).
cnf(c_4051,plain,
( familiar(n3,n1)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7032]) ).
cnf(c_4061,plain,
( ~ familiar(A,n3)
| ~ familiar(n1,A)
| familiar(n1,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_4051,c_63]) ).
cnf(c_7033,plain,
( familiar(n3,n2)
| familiar(n2,n5)
| familiar(n3,n2)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_2638,c_798]) ).
cnf(c_7034,plain,
( familiar(n3,n2)
| familiar(n3,n2)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(copy,[status(thm)],[c_7033]) ).
cnf(c_4104,plain,
( familiar(n3,n2)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(copy,[status(thm)],[c_7034]) ).
cnf(c_7035,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_2691,c_801]) ).
cnf(c_7036,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7035]) ).
cnf(c_4193,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7036]) ).
cnf(c_7037,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| familiar(n1,n3)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolve,[status(thm)],[c_2697,c_797]) ).
cnf(c_7038,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7037]) ).
cnf(c_4218,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(copy,[status(thm)],[c_7038]) ).
cnf(c_4227,plain,
( ~ familiar(A,n4)
| ~ familiar(n1,A)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_4218,c_63]) ).
cnf(c_7039,plain,
( familiar(n2,n3)
| familiar(n2,n5)
| familiar(n2,n3)
| familiar(n2,n5)
| familiar(n4,n2) ),
inference(resolve,[status(thm)],[c_2721,c_799]) ).
cnf(c_7040,plain,
( familiar(n2,n3)
| familiar(n2,n3)
| familiar(n2,n5)
| familiar(n4,n2) ),
inference(copy,[status(thm)],[c_7039]) ).
cnf(c_4250,plain,
( familiar(n2,n3)
| familiar(n2,n5)
| familiar(n4,n2) ),
inference(copy,[status(thm)],[c_7040]) ).
cnf(c_7041,plain,
( familiar(n2,n1)
| familiar(n1,n5)
| familiar(n2,n1)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_2767,c_800]) ).
cnf(c_7042,plain,
( familiar(n2,n1)
| familiar(n2,n1)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7041]) ).
cnf(c_4268,plain,
( familiar(n2,n1)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7042]) ).
cnf(c_4277,plain,
( familiar(n1,n3)
| familiar(n2,n1)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_4268,c_65]) ).
cnf(c_7043,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_2769,c_801]) ).
cnf(c_7044,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7043]) ).
cnf(c_4324,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7044]) ).
cnf(c_4333,plain,
( ~ familiar(A,n3)
| ~ familiar(n1,A)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_4324,c_63]) ).
cnf(c_7045,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(resolve,[status(thm)],[c_3009,c_825]) ).
cnf(c_7046,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7045]) ).
cnf(c_4446,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(copy,[status(thm)],[c_7046]) ).
cnf(c_7047,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| ~ familiar(n6,n3)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_3085,c_4324]) ).
cnf(c_7048,plain,
( familiar(n1,n2)
| ~ familiar(n6,n3)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7047]) ).
cnf(c_4489,plain,
( ~ familiar(n6,n3)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7048]) ).
cnf(c_7049,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| ~ familiar(n6,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_3085,c_4193]) ).
cnf(c_7050,plain,
( familiar(n1,n2)
| ~ familiar(n6,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7049]) ).
cnf(c_4490,plain,
( ~ familiar(n6,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7050]) ).
cnf(c_4500,plain,
( familiar(n3,n4)
| familiar(n6,n3)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_4490,c_631]) ).
cnf(c_7051,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| ~ familiar(n6,n2)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_3125,c_4277]) ).
cnf(c_7052,plain,
( familiar(n1,n3)
| ~ familiar(n6,n2)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7051]) ).
cnf(c_4526,plain,
( ~ familiar(n6,n2)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7052]) ).
cnf(c_7053,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| ~ familiar(n6,n4)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_3125,c_4218]) ).
cnf(c_7054,plain,
( familiar(n1,n3)
| ~ familiar(n6,n4)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7053]) ).
cnf(c_4527,plain,
( ~ familiar(n6,n4)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7054]) ).
cnf(c_4539,plain,
( familiar(n2,n4)
| familiar(n6,n2)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_4527,c_630]) ).
cnf(c_7055,plain,
( familiar(n1,n5)
| familiar(n1,n4)
| ~ familiar(n6,n3)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_3175,c_4051]) ).
cnf(c_7056,plain,
( familiar(n1,n5)
| ~ familiar(n6,n3)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7055]) ).
cnf(c_4552,plain,
( ~ familiar(n6,n3)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7056]) ).
cnf(c_7057,plain,
( familiar(n1,n5)
| familiar(n1,n4)
| ~ familiar(n6,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_3175,c_4007]) ).
cnf(c_7058,plain,
( familiar(n1,n5)
| ~ familiar(n6,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7057]) ).
cnf(c_4553,plain,
( ~ familiar(n6,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7058]) ).
cnf(c_4558,plain,
( familiar(n2,n3)
| familiar(n6,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_4552,c_643]) ).
cnf(c_7059,plain,
( familiar(n2,n3)
| familiar(n2,n5)
| ~ familiar(n6,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_3257,c_4250]) ).
cnf(c_7060,plain,
( familiar(n2,n3)
| ~ familiar(n6,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(copy,[status(thm)],[c_7059]) ).
cnf(c_4592,plain,
( ~ familiar(n6,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(copy,[status(thm)],[c_7060]) ).
cnf(c_4595,plain,
( familiar(n1,n4)
| familiar(n6,n1)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_4592,c_629]) ).
cnf(c_7061,plain,
( familiar(n2,n5)
| familiar(n2,n4)
| ~ familiar(n6,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_3318,c_4104]) ).
cnf(c_7062,plain,
( familiar(n2,n5)
| ~ familiar(n6,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(copy,[status(thm)],[c_7061]) ).
cnf(c_4624,plain,
( ~ familiar(n6,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(copy,[status(thm)],[c_7062]) ).
cnf(c_4635,plain,
( familiar(n1,n3)
| familiar(n6,n1)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_4624,c_642]) ).
cnf(c_7063,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| ~ familiar(n6,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_3539,c_4446]) ).
cnf(c_7064,plain,
( familiar(n1,n2)
| ~ familiar(n6,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7063]) ).
cnf(c_4717,plain,
( ~ familiar(n6,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7064]) ).
cnf(c_4720,plain,
( familiar(n5,n3)
| familiar(n5,n6)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_4717,c_647]) ).
cnf(c_7065,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| ~ familiar(n5,n6)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_3542,c_4014]) ).
cnf(c_7066,plain,
( familiar(n1,n2)
| ~ familiar(n5,n6)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7065]) ).
cnf(c_4732,plain,
( ~ familiar(n5,n6)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7066]) ).
cnf(c_7067,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_4038,c_4446]) ).
cnf(c_7068,plain,
( familiar(n1,n2)
| ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7067]) ).
cnf(c_5168,plain,
( ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7068]) ).
cnf(c_7069,plain,
( familiar(n1,n5)
| familiar(n1,n2)
| familiar(n3,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_4500,c_4489]) ).
cnf(c_7070,plain,
( familiar(n1,n5)
| familiar(n3,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7069]) ).
cnf(c_5341,plain,
( familiar(n3,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7070]) ).
cnf(c_5343,plain,
( familiar(n4,n3)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5341,c_65]) ).
cnf(c_7071,plain,
( ~ familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5343,c_4333]) ).
cnf(c_7072,plain,
( ~ familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7071]) ).
cnf(c_5345,plain,
( ~ familiar(n1,n4)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7072]) ).
cnf(c_7073,plain,
( familiar(n1,n5)
| familiar(n1,n3)
| familiar(n2,n4)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_4539,c_4526]) ).
cnf(c_7074,plain,
( familiar(n1,n5)
| familiar(n2,n4)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7073]) ).
cnf(c_5460,plain,
( familiar(n2,n4)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7074]) ).
cnf(c_7075,plain,
( ~ familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_5460,c_4227]) ).
cnf(c_7076,plain,
( ~ familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7075]) ).
cnf(c_5462,plain,
( ~ familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7076]) ).
cnf(c_7077,plain,
( familiar(n1,n4)
| familiar(n1,n5)
| familiar(n2,n3)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_4558,c_4553]) ).
cnf(c_7078,plain,
( familiar(n1,n4)
| familiar(n2,n3)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7077]) ).
cnf(c_5539,plain,
( familiar(n2,n3)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7078]) ).
cnf(c_7079,plain,
( ~ familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n4)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_5539,c_4061]) ).
cnf(c_7080,plain,
( ~ familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7079]) ).
cnf(c_5540,plain,
( ~ familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(copy,[status(thm)],[c_7080]) ).
cnf(c_7081,plain,
( ~ familiar(n1,n2)
| familiar(n2,n5)
| familiar(n2,n3)
| familiar(n1,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_4595,c_3257]) ).
cnf(c_7082,plain,
( ~ familiar(n1,n2)
| familiar(n2,n5)
| familiar(n1,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(copy,[status(thm)],[c_7081]) ).
cnf(c_5668,plain,
( ~ familiar(n1,n2)
| familiar(n1,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(copy,[status(thm)],[c_7082]) ).
cnf(c_7083,plain,
( ~ familiar(n1,n2)
| familiar(n2,n4)
| familiar(n2,n5)
| familiar(n1,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_4635,c_3318]) ).
cnf(c_7084,plain,
( ~ familiar(n1,n2)
| familiar(n2,n4)
| familiar(n1,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(copy,[status(thm)],[c_7083]) ).
cnf(c_5757,plain,
( ~ familiar(n1,n2)
| familiar(n1,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(copy,[status(thm)],[c_7084]) ).
cnf(c_7085,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_4720,c_4732]) ).
cnf(c_7086,plain,
( familiar(n1,n2)
| familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7085]) ).
cnf(c_5804,plain,
( familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7086]) ).
cnf(c_7087,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_5804,c_5168]) ).
cnf(c_7088,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7087]) ).
cnf(c_5806,plain,
( familiar(n1,n2)
| familiar(n1,n4) ),
inference(copy,[status(thm)],[c_7088]) ).
cnf(c_7089,plain,
( familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5806,c_5345]) ).
cnf(c_5807,plain,
( familiar(n1,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7089]) ).
cnf(c_7090,plain,
( ~ familiar(n4,n3)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5806,c_3851]) ).
cnf(c_5808,plain,
( ~ familiar(n4,n3)
| familiar(n1,n6)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7090]) ).
cnf(c_5839,plain,
( familiar(n4,n1)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5806,c_65]) ).
cnf(c_5840,plain,
( ~ familiar(A,n1)
| ~ familiar(n4,A)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5806,c_63]) ).
cnf(c_7091,plain,
( ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5807,c_3851]) ).
cnf(c_5841,plain,
( ~ familiar(n5,n3)
| familiar(n1,n6)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7091]) ).
cnf(c_5877,plain,
( familiar(n5,n1)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5807,c_65]) ).
cnf(c_5878,plain,
( ~ familiar(A,n1)
| ~ familiar(n5,A)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5807,c_63]) ).
cnf(c_5891,plain,
( ~ familiar(A,n4)
| ~ familiar(n1,A)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5839,c_63]) ).
cnf(c_5903,plain,
( ~ familiar(A,n5)
| ~ familiar(n1,A)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5877,c_63]) ).
cnf(c_7092,plain,
( familiar(n1,n2)
| ~ familiar(n4,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5840,c_5877]) ).
cnf(c_6006,plain,
( ~ familiar(n4,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7092]) ).
cnf(c_7093,plain,
( familiar(n1,n2)
| ~ familiar(n5,n4)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_5878,c_5839]) ).
cnf(c_6091,plain,
( ~ familiar(n5,n4)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7093]) ).
cnf(c_6092,plain,
( familiar(n5,n3)
| familiar(n4,n3)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6091,c_762]) ).
cnf(c_7094,plain,
( familiar(n1,n6)
| familiar(n1,n2)
| familiar(n4,n3)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6092,c_5841]) ).
cnf(c_6126,plain,
( familiar(n1,n6)
| familiar(n4,n3)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7094]) ).
cnf(c_7095,plain,
( familiar(n1,n6)
| familiar(n1,n2)
| familiar(n1,n6)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6126,c_5808]) ).
cnf(c_7096,plain,
( familiar(n1,n6)
| familiar(n1,n6)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7095]) ).
cnf(c_6204,plain,
( familiar(n1,n6)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7096]) ).
cnf(c_7097,plain,
( ~ familiar(n6,n5)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6204,c_5903]) ).
cnf(c_6206,plain,
( ~ familiar(n6,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7097]) ).
cnf(c_7098,plain,
( ~ familiar(n6,n4)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6204,c_5891]) ).
cnf(c_6207,plain,
( ~ familiar(n6,n4)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7098]) ).
cnf(c_6251,plain,
( familiar(n4,n5)
| familiar(n6,n4)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6206,c_574]) ).
cnf(c_7099,plain,
( familiar(n1,n2)
| familiar(n4,n5)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6251,c_6207]) ).
cnf(c_6290,plain,
( familiar(n4,n5)
| familiar(n1,n2) ),
inference(copy,[status(thm)],[c_7099]) ).
cnf(c_7100,plain,
( familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolve,[status(thm)],[c_6290,c_6006]) ).
cnf(c_6291,plain,
familiar(n1,n2),
inference(copy,[status(thm)],[c_7100]) ).
cnf(c_6293,plain,
( familiar(n1,n3)
| familiar(n2,n4)
| familiar(n2,n5) ),
inference(resolve,[status(thm)],[c_6291,c_5757]) ).
cnf(c_6296,plain,
( familiar(n1,n4)
| familiar(n2,n5)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_6291,c_5668]) ).
cnf(c_6298,plain,
( familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolve,[status(thm)],[c_6291,c_5540]) ).
cnf(c_6299,plain,
( familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6291,c_5462]) ).
cnf(c_6354,plain,
familiar(n2,n1),
inference(resolve,[status(thm)],[c_6291,c_65]) ).
cnf(c_6355,plain,
( ~ familiar(A,n1)
| ~ familiar(n2,A) ),
inference(resolve,[status(thm)],[c_6291,c_63]) ).
cnf(c_6384,plain,
( ~ familiar(A,n2)
| ~ familiar(n1,A) ),
inference(resolve,[status(thm)],[c_6354,c_63]) ).
cnf(c_6416,plain,
( familiar(n5,n1)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_6298,c_65]) ).
cnf(c_7101,plain,
( ~ familiar(n2,n1)
| familiar(n2,n3)
| familiar(n2,n6)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6299,c_3234]) ).
cnf(c_6424,plain,
( familiar(n2,n3)
| familiar(n2,n6)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6354,c_7101]) ).
cnf(c_6452,plain,
( familiar(n5,n1)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6299,c_65]) ).
cnf(c_6458,plain,
( ~ familiar(n2,n5)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_6416,c_6355]) ).
cnf(c_6470,plain,
( ~ familiar(n2,n5)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6452,c_6355]) ).
cnf(c_7102,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n2,n4) ),
inference(resolve,[status(thm)],[c_6293,c_6470]) ).
cnf(c_6495,plain,
( familiar(n1,n3)
| familiar(n2,n4) ),
inference(copy,[status(thm)],[c_7102]) ).
cnf(c_7103,plain,
( ~ familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n6)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6495,c_3618]) ).
cnf(c_7104,plain,
( ~ familiar(n1,n2)
| familiar(n1,n6)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7103]) ).
cnf(c_6497,plain,
( familiar(n1,n6)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6291,c_7104]) ).
cnf(c_7105,plain,
( ~ familiar(n3,n2)
| familiar(n1,n4)
| familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6495,c_963]) ).
cnf(c_6507,plain,
( ~ familiar(n3,n2)
| familiar(n1,n4)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7105]) ).
cnf(c_6514,plain,
( familiar(n4,n2)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6495,c_65]) ).
cnf(c_6558,plain,
( familiar(n6,n1)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6497,c_65]) ).
cnf(c_6571,plain,
( ~ familiar(n1,n4)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6514,c_6384]) ).
cnf(c_6576,plain,
( ~ familiar(n2,n6)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6558,c_6355]) ).
cnf(c_7106,plain,
( familiar(n1,n4)
| familiar(n1,n4)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_6296,c_6458]) ).
cnf(c_6590,plain,
( familiar(n1,n4)
| familiar(n2,n3) ),
inference(copy,[status(thm)],[c_7106]) ).
cnf(c_6603,plain,
( familiar(n3,n2)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_6590,c_65]) ).
cnf(c_6649,plain,
( ~ familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolve,[status(thm)],[c_6603,c_6384]) ).
cnf(c_7107,plain,
( familiar(n1,n3)
| familiar(n2,n3)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6424,c_6576]) ).
cnf(c_6693,plain,
( familiar(n2,n3)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7107]) ).
cnf(c_6696,plain,
( familiar(n3,n2)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6693,c_65]) ).
cnf(c_7108,plain,
( familiar(n1,n3)
| familiar(n1,n4)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6507,c_6696]) ).
cnf(c_6728,plain,
( familiar(n1,n4)
| familiar(n1,n3) ),
inference(copy,[status(thm)],[c_7108]) ).
cnf(c_7109,plain,
( familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolve,[status(thm)],[c_6728,c_6571]) ).
cnf(c_6729,plain,
familiar(n1,n3),
inference(copy,[status(thm)],[c_7109]) ).
cnf(c_6730,plain,
familiar(n1,n4),
inference(resolve,[status(thm)],[c_6729,c_6649]) ).
cnf(c_6783,plain,
familiar(n3,n1),
inference(resolve,[status(thm)],[c_6729,c_65]) ).
cnf(c_6910,plain,
~ familiar(n4,n2),
inference(resolve,[status(thm)],[c_6730,c_6384]) ).
cnf(c_7110,plain,
( ~ familiar(n3,n1)
| familiar(n4,n2)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_6730,c_964]) ).
cnf(c_7111,plain,
( ~ familiar(n3,n1)
| familiar(n2,n3) ),
inference(resolve,[status(thm)],[c_6910,c_7110]) ).
cnf(c_6912,plain,
familiar(n2,n3),
inference(resolve,[status(thm)],[c_6783,c_7111]) ).
cnf(c_7112,plain,
~ familiar(n2,n3),
inference(resolve,[status(thm)],[c_6783,c_6355]) ).
cnf(c_6965,plain,
$false,
inference(resolve,[status(thm)],[c_6912,c_7112]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ028-6 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 05:05:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3828728 was started by sandbox2 on n011,
% 0.09/0.37 % Sat Sep 26 05:05:43 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 15.52/2.42
% 15.52/2.42 % given #500 (W,wt=14): 561 familiar(n6,n5) | -not_familiar(n6,n4) | familiar(n5,n4). [resolve(164,c,124,b)].
% 15.52/2.42
% 15.52/2.42 % given #1000 (T,wt=14): 3268 familiar(n2,n6) | familiar(n3,n2) | familiar(n2,n5). [resolve(3263,a,65,a)].
% 15.52/2.42
% 15.52/2.42 % given #1500 (W,wt=17): 2562 familiar(n1,n6) | familiar(n2,n1) | -familiar(n6,n3) | familiar(n1,n3). [resolve(912,d,829,a),merge(d)].
% 15.52/2.42
% 15.52/2.42 % given #2000 (T,wt=17): 3808 familiar(n1,n3) | familiar(n1,n2) | familiar(n3,n6) | familiar(n3,n5). [resolve(3791,a,1353,c),merge(e)].
% 15.52/2.42
% 15.52/2.42 % given #2500 (A,wt=20): 1632 familiar(n4,n2) | familiar(n2,n6) | -familiar(n3,n6) | familiar(n3,n1) | familiar(n1,n4). [resolve(853,c,807,a)].
% 15.52/2.42
% 15.52/2.42 % SZS status Unsatisfiable for theBenchmark
% 15.52/2.42
% 15.52/2.42 % Proof 1 at 1.51 (+ 0.44) seconds.
% 15.52/2.42 % Length of proof is 371.
% 15.52/2.42 % Level of proof is 40.
% 15.52/2.42 % Maximum clause weight is 17.000.
% 15.52/2.42 % Given clauses 2659.
% 15.52/2.42
% 15.52/2.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------