%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ028-5 : 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 : n018.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 0.13s 0.48s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 15
% Syntax : Number of formulae : 354 ( 40 unt; 0 def)
% Number of atoms : 1151 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 1056 ( 259 ~; 797 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 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 : 68 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(person1,axiom,
person(one),
file('theBenchmark.p',person1) ).
cnf(c_1,plain,
person(one),
inference(clausify,[status(thm)],[person1]) ).
fof(person2,axiom,
person(two),
file('theBenchmark.p',person2) ).
cnf(c_2,plain,
person(two),
inference(clausify,[status(thm)],[person2]) ).
fof(person3,axiom,
person(three),
file('theBenchmark.p',person3) ).
cnf(c_3,plain,
person(three),
inference(clausify,[status(thm)],[person3]) ).
fof(person4,axiom,
person(four),
file('theBenchmark.p',person4) ).
cnf(c_4,plain,
person(four),
inference(clausify,[status(thm)],[person4]) ).
fof(person5,axiom,
person(five),
file('theBenchmark.p',person5) ).
cnf(c_5,plain,
person(five),
inference(clausify,[status(thm)],[person5]) ).
fof(person6,axiom,
person(six),
file('theBenchmark.p',person6) ).
cnf(c_6,plain,
person(six),
inference(clausify,[status(thm)],[person6]) ).
fof(order1,axiom,
after(one,two),
file('theBenchmark.p',order1) ).
cnf(c_7,plain,
after(one,two),
inference(clausify,[status(thm)],[order1]) ).
fof(order2,axiom,
after(two,three),
file('theBenchmark.p',order2) ).
cnf(c_8,plain,
after(two,three),
inference(clausify,[status(thm)],[order2]) ).
fof(order3,axiom,
after(three,four),
file('theBenchmark.p',order3) ).
cnf(c_9,plain,
after(three,four),
inference(clausify,[status(thm)],[order3]) ).
fof(order4,axiom,
after(four,five),
file('theBenchmark.p',order4) ).
cnf(c_10,plain,
after(four,five),
inference(clausify,[status(thm)],[order4]) ).
fof(order5,axiom,
after(five,six),
file('theBenchmark.p',order5) ).
cnf(c_11,plain,
after(five,six),
inference(clausify,[status(thm)],[order5]) ).
fof(transitivity_of_order,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ after(VAR_2,VAR_1)
| ~ after(VAR_0,VAR_2)
| after(VAR_0,VAR_1) ),
file('theBenchmark.p',transitivity_of_order) ).
cnf(c_12,plain,
( ~ after(C,B)
| ~ after(A,C)
| after(A,B) ),
inference(clausify,[status(thm)],[transitivity_of_order]) ).
fof(familiar_or_not,axiom,
! [VAR_0,VAR_1] :
( ~ after(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_13,plain,
( ~ after(A,B)
| ~ person(B)
| ~ person(A)
| not_familiar(A,B)
| familiar(A,B) ),
inference(clausify,[status(thm)],[familiar_or_not]) ).
fof(three_familiar,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ familiar(VAR_0,VAR_2)
| ~ familiar(VAR_1,VAR_2)
| ~ familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',three_familiar) ).
cnf(c_14,plain,
( ~ familiar(A,C)
| ~ familiar(B,C)
| ~ familiar(A,B) ),
inference(clausify,[status(thm)],[three_familiar]) ).
fof(three_not_familiar,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ not_familiar(VAR_0,VAR_2)
| ~ not_familiar(VAR_1,VAR_2)
| ~ not_familiar(VAR_0,VAR_1) ),
file('theBenchmark.p',three_not_familiar) ).
cnf(c_15,plain,
( ~ not_familiar(A,C)
| ~ not_familiar(B,C)
| ~ not_familiar(A,B) ),
inference(clausify,[status(thm)],[three_not_familiar]) ).
cnf(c_21,plain,
( ~ after(five,A)
| after(four,A) ),
inference(resolve,[status(thm)],[c_12,c_10]) ).
cnf(c_22,plain,
( ~ after(four,A)
| after(three,A) ),
inference(resolve,[status(thm)],[c_12,c_9]) ).
cnf(c_23,plain,
( ~ after(three,A)
| after(two,A) ),
inference(resolve,[status(thm)],[c_12,c_8]) ).
cnf(c_24,plain,
( ~ after(two,A)
| after(one,A) ),
inference(resolve,[status(thm)],[c_12,c_7]) ).
cnf(c_1058,plain,
( ~ person(six)
| ~ person(five)
| not_familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_13,c_11]) ).
cnf(c_1059,plain,
( ~ person(six)
| not_familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_5,c_1058]) ).
cnf(c_30,plain,
( not_familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_6,c_1059]) ).
cnf(c_1060,plain,
( ~ person(five)
| ~ person(four)
| not_familiar(four,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_13,c_10]) ).
cnf(c_1061,plain,
( ~ person(five)
| not_familiar(four,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_4,c_1060]) ).
cnf(c_31,plain,
( not_familiar(four,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_5,c_1061]) ).
cnf(c_1062,plain,
( ~ person(four)
| ~ person(three)
| not_familiar(three,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_13,c_9]) ).
cnf(c_1063,plain,
( ~ person(four)
| not_familiar(three,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_3,c_1062]) ).
cnf(c_32,plain,
( not_familiar(three,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_4,c_1063]) ).
cnf(c_1064,plain,
( ~ person(three)
| ~ person(two)
| not_familiar(two,three)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_13,c_8]) ).
cnf(c_1065,plain,
( ~ person(three)
| not_familiar(two,three)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_2,c_1064]) ).
cnf(c_33,plain,
( not_familiar(two,three)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_3,c_1065]) ).
cnf(c_1066,plain,
( ~ person(two)
| ~ person(one)
| not_familiar(one,two)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_13,c_7]) ).
cnf(c_1067,plain,
( ~ person(two)
| not_familiar(one,two)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_1,c_1066]) ).
cnf(c_34,plain,
( not_familiar(one,two)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_2,c_1067]) ).
cnf(c_45,plain,
after(four,six),
inference(resolve,[status(thm)],[c_21,c_11]) ).
cnf(c_1068,plain,
( ~ person(six)
| ~ person(four)
| not_familiar(four,six)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_45,c_13]) ).
cnf(c_1069,plain,
( ~ person(six)
| not_familiar(four,six)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_4,c_1068]) ).
cnf(c_46,plain,
( not_familiar(four,six)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_6,c_1069]) ).
cnf(c_50,plain,
after(three,six),
inference(resolve,[status(thm)],[c_22,c_45]) ).
cnf(c_51,plain,
after(three,five),
inference(resolve,[status(thm)],[c_22,c_10]) ).
cnf(c_1070,plain,
( ~ person(six)
| ~ person(three)
| not_familiar(three,six)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_50,c_13]) ).
cnf(c_1071,plain,
( ~ person(six)
| not_familiar(three,six)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_3,c_1070]) ).
cnf(c_52,plain,
( not_familiar(three,six)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_6,c_1071]) ).
cnf(c_56,plain,
after(two,six),
inference(resolve,[status(thm)],[c_23,c_50]) ).
cnf(c_57,plain,
after(two,four),
inference(resolve,[status(thm)],[c_23,c_9]) ).
cnf(c_60,plain,
after(two,five),
inference(resolve,[status(thm)],[c_51,c_23]) ).
cnf(c_1072,plain,
( ~ person(five)
| ~ person(three)
| not_familiar(three,five)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_51,c_13]) ).
cnf(c_1073,plain,
( ~ person(five)
| not_familiar(three,five)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_3,c_1072]) ).
cnf(c_61,plain,
( not_familiar(three,five)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_5,c_1073]) ).
cnf(c_1074,plain,
( ~ person(six)
| ~ person(two)
| not_familiar(two,six)
| familiar(two,six) ),
inference(resolve,[status(thm)],[c_56,c_13]) ).
cnf(c_1075,plain,
( ~ person(six)
| not_familiar(two,six)
| familiar(two,six) ),
inference(resolve,[status(thm)],[c_2,c_1074]) ).
cnf(c_64,plain,
( not_familiar(two,six)
| familiar(two,six) ),
inference(resolve,[status(thm)],[c_6,c_1075]) ).
cnf(c_1076,plain,
( ~ person(four)
| ~ person(two)
| not_familiar(two,four)
| familiar(two,four) ),
inference(resolve,[status(thm)],[c_57,c_13]) ).
cnf(c_1077,plain,
( ~ person(four)
| not_familiar(two,four)
| familiar(two,four) ),
inference(resolve,[status(thm)],[c_2,c_1076]) ).
cnf(c_68,plain,
( not_familiar(two,four)
| familiar(two,four) ),
inference(resolve,[status(thm)],[c_4,c_1077]) ).
cnf(c_1078,plain,
( ~ person(five)
| ~ person(two)
| not_familiar(two,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_60,c_13]) ).
cnf(c_1079,plain,
( ~ person(five)
| not_familiar(two,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_2,c_1078]) ).
cnf(c_73,plain,
( not_familiar(two,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_5,c_1079]) ).
cnf(c_76,plain,
after(one,five),
inference(resolve,[status(thm)],[c_24,c_60]) ).
cnf(c_77,plain,
after(one,four),
inference(resolve,[status(thm)],[c_24,c_57]) ).
cnf(c_78,plain,
after(one,six),
inference(resolve,[status(thm)],[c_24,c_56]) ).
cnf(c_79,plain,
after(one,three),
inference(resolve,[status(thm)],[c_24,c_8]) ).
cnf(c_1080,plain,
( ~ person(five)
| ~ person(one)
| not_familiar(one,five)
| familiar(one,five) ),
inference(resolve,[status(thm)],[c_76,c_13]) ).
cnf(c_1081,plain,
( ~ person(five)
| not_familiar(one,five)
| familiar(one,five) ),
inference(resolve,[status(thm)],[c_1,c_1080]) ).
cnf(c_81,plain,
( not_familiar(one,five)
| familiar(one,five) ),
inference(resolve,[status(thm)],[c_5,c_1081]) ).
cnf(c_1082,plain,
( ~ person(four)
| ~ person(one)
| not_familiar(one,four)
| familiar(one,four) ),
inference(resolve,[status(thm)],[c_77,c_13]) ).
cnf(c_1083,plain,
( ~ person(four)
| not_familiar(one,four)
| familiar(one,four) ),
inference(resolve,[status(thm)],[c_1,c_1082]) ).
cnf(c_86,plain,
( not_familiar(one,four)
| familiar(one,four) ),
inference(resolve,[status(thm)],[c_4,c_1083]) ).
cnf(c_1084,plain,
( ~ person(six)
| ~ person(one)
| not_familiar(one,six)
| familiar(one,six) ),
inference(resolve,[status(thm)],[c_78,c_13]) ).
cnf(c_1085,plain,
( ~ person(six)
| not_familiar(one,six)
| familiar(one,six) ),
inference(resolve,[status(thm)],[c_1,c_1084]) ).
cnf(c_90,plain,
( not_familiar(one,six)
| familiar(one,six) ),
inference(resolve,[status(thm)],[c_6,c_1085]) ).
cnf(c_1086,plain,
( ~ person(three)
| ~ person(one)
| not_familiar(one,three)
| familiar(one,three) ),
inference(resolve,[status(thm)],[c_79,c_13]) ).
cnf(c_1087,plain,
( ~ person(three)
| not_familiar(one,three)
| familiar(one,three) ),
inference(resolve,[status(thm)],[c_1,c_1086]) ).
cnf(c_93,plain,
( not_familiar(one,three)
| familiar(one,three) ),
inference(resolve,[status(thm)],[c_3,c_1087]) ).
cnf(c_97,plain,
( ~ not_familiar(A,six)
| ~ not_familiar(A,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_30,c_15]) ).
cnf(c_100,plain,
( ~ not_familiar(A,five)
| ~ not_familiar(A,four)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_31,c_15]) ).
cnf(c_103,plain,
( ~ not_familiar(A,four)
| ~ not_familiar(A,three)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_32,c_15]) ).
cnf(c_104,plain,
( ~ not_familiar(three,A)
| ~ not_familiar(four,A)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_32,c_15]) ).
cnf(c_106,plain,
( ~ not_familiar(A,three)
| ~ not_familiar(A,two)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_33,c_15]) ).
cnf(c_107,plain,
( ~ not_familiar(two,A)
| ~ not_familiar(three,A)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_33,c_15]) ).
cnf(c_110,plain,
( ~ not_familiar(one,A)
| ~ not_familiar(two,A)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_34,c_15]) ).
cnf(c_112,plain,
( ~ not_familiar(A,six)
| ~ not_familiar(A,four)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_46,c_15]) ).
cnf(c_115,plain,
( ~ not_familiar(A,six)
| ~ not_familiar(A,three)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_52,c_15]) ).
cnf(c_118,plain,
( ~ not_familiar(A,five)
| ~ not_familiar(A,three)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_61,c_15]) ).
cnf(c_145,plain,
( familiar(one,six)
| ~ not_familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_97,c_90]) ).
cnf(c_146,plain,
( familiar(two,six)
| ~ not_familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_97,c_64]) ).
cnf(c_147,plain,
( familiar(three,six)
| ~ not_familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_97,c_52]) ).
cnf(c_148,plain,
( familiar(four,six)
| ~ not_familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_97,c_46]) ).
cnf(c_153,plain,
( familiar(one,four)
| ~ not_familiar(one,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_100,c_86]) ).
cnf(c_154,plain,
( familiar(two,four)
| ~ not_familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_100,c_68]) ).
cnf(c_155,plain,
( familiar(three,four)
| ~ not_familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_100,c_32]) ).
cnf(c_161,plain,
( familiar(one,three)
| ~ not_familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_103,c_93]) ).
cnf(c_162,plain,
( familiar(two,three)
| ~ not_familiar(two,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_103,c_33]) ).
cnf(c_164,plain,
( familiar(three,six)
| ~ not_familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_104,c_52]) ).
cnf(c_169,plain,
( familiar(one,two)
| ~ not_familiar(one,three)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_106,c_34]) ).
cnf(c_170,plain,
( familiar(two,five)
| ~ not_familiar(three,five)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_107,c_73]) ).
cnf(c_172,plain,
( familiar(two,six)
| ~ not_familiar(three,six)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_107,c_64]) ).
cnf(c_178,plain,
( familiar(one,six)
| ~ not_familiar(two,six)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_110,c_90]) ).
cnf(c_179,plain,
( familiar(one,four)
| ~ not_familiar(two,four)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_110,c_86]) ).
cnf(c_180,plain,
( familiar(one,five)
| ~ not_familiar(two,five)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_110,c_81]) ).
cnf(c_184,plain,
( familiar(one,six)
| ~ not_familiar(one,four)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_112,c_90]) ).
cnf(c_185,plain,
( familiar(two,six)
| ~ not_familiar(two,four)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_112,c_64]) ).
cnf(c_190,plain,
( familiar(one,six)
| ~ not_familiar(one,three)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_115,c_90]) ).
cnf(c_196,plain,
( familiar(one,three)
| ~ not_familiar(one,five)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_118,c_93]) ).
cnf(c_231,plain,
( familiar(one,five)
| familiar(one,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_145,c_81]) ).
cnf(c_232,plain,
( familiar(two,five)
| familiar(two,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_146,c_73]) ).
cnf(c_233,plain,
( familiar(three,five)
| familiar(three,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_147,c_61]) ).
cnf(c_234,plain,
( familiar(four,five)
| familiar(four,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_148,c_31]) ).
cnf(c_235,plain,
( familiar(one,five)
| familiar(one,four)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_153,c_81]) ).
cnf(c_236,plain,
( familiar(two,five)
| familiar(two,four)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_154,c_73]) ).
cnf(c_237,plain,
( familiar(three,five)
| familiar(three,four)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_155,c_61]) ).
cnf(c_238,plain,
( familiar(one,four)
| familiar(one,three)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_161,c_86]) ).
cnf(c_239,plain,
( familiar(two,four)
| familiar(two,three)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_162,c_68]) ).
cnf(c_240,plain,
( familiar(four,six)
| familiar(three,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_164,c_46]) ).
cnf(c_241,plain,
( familiar(one,three)
| familiar(one,two)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_169,c_93]) ).
cnf(c_242,plain,
( familiar(three,five)
| familiar(two,five)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_170,c_61]) ).
cnf(c_243,plain,
( familiar(three,six)
| familiar(two,six)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_172,c_52]) ).
cnf(c_244,plain,
( familiar(two,six)
| familiar(one,six)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_178,c_64]) ).
cnf(c_245,plain,
( familiar(two,four)
| familiar(one,four)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_179,c_68]) ).
cnf(c_246,plain,
( familiar(two,five)
| familiar(one,five)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_180,c_73]) ).
cnf(c_247,plain,
( familiar(one,four)
| familiar(one,six)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_184,c_86]) ).
cnf(c_248,plain,
( familiar(two,four)
| familiar(two,six)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_185,c_68]) ).
cnf(c_249,plain,
( familiar(one,three)
| familiar(one,six)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_190,c_93]) ).
cnf(c_250,plain,
( familiar(one,five)
| familiar(one,three)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_196,c_81]) ).
cnf(c_251,plain,
( ~ familiar(A,six)
| ~ familiar(one,A)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_231,c_14]) ).
cnf(c_254,plain,
( ~ familiar(A,six)
| ~ familiar(two,A)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_232,c_14]) ).
cnf(c_257,plain,
( ~ familiar(A,six)
| ~ familiar(three,A)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_233,c_14]) ).
cnf(c_263,plain,
( ~ familiar(A,four)
| ~ familiar(one,A)
| familiar(one,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_235,c_14]) ).
cnf(c_266,plain,
( ~ familiar(A,four)
| ~ familiar(two,A)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_236,c_14]) ).
cnf(c_272,plain,
( ~ familiar(A,three)
| ~ familiar(one,A)
| familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_238,c_14]) ).
cnf(c_274,plain,
( ~ familiar(one,A)
| ~ familiar(three,A)
| familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_238,c_14]) ).
cnf(c_277,plain,
( ~ familiar(two,A)
| ~ familiar(three,A)
| familiar(two,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_239,c_14]) ).
cnf(c_285,plain,
( ~ familiar(A,three)
| ~ familiar(A,two)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_242,c_14]) ).
cnf(c_287,plain,
( ~ familiar(A,six)
| ~ familiar(two,A)
| familiar(three,six)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_243,c_14]) ).
cnf(c_290,plain,
( ~ familiar(A,six)
| ~ familiar(one,A)
| familiar(two,six)
| familiar(one,two) ),
inference(resolve,[status(thm)],[c_244,c_14]) ).
cnf(c_299,plain,
( ~ familiar(A,six)
| ~ familiar(one,A)
| familiar(one,four)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_247,c_14]) ).
cnf(c_302,plain,
( ~ familiar(A,six)
| ~ familiar(two,A)
| familiar(two,four)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_248,c_14]) ).
cnf(c_305,plain,
( ~ familiar(A,six)
| ~ familiar(one,A)
| familiar(one,three)
| familiar(three,six) ),
inference(resolve,[status(thm)],[c_249,c_14]) ).
cnf(c_1088,plain,
( familiar(one,five)
| familiar(three,five)
| ~ familiar(three,six)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_251,c_250]) ).
cnf(c_311,plain,
( familiar(three,five)
| ~ familiar(three,six)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1088]) ).
cnf(c_1089,plain,
( familiar(two,five)
| familiar(one,five)
| ~ familiar(two,six)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_251,c_246]) ).
cnf(c_312,plain,
( familiar(two,five)
| ~ familiar(two,six)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1089]) ).
cnf(c_1090,plain,
( familiar(one,five)
| familiar(four,five)
| ~ familiar(four,six)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_251,c_235]) ).
cnf(c_316,plain,
( familiar(four,five)
| ~ familiar(four,six)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1090]) ).
cnf(c_1091,plain,
( familiar(three,five)
| familiar(two,five)
| ~ familiar(three,six)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_254,c_242]) ).
cnf(c_329,plain,
( familiar(three,five)
| ~ familiar(three,six)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1091]) ).
cnf(c_1092,plain,
( familiar(two,five)
| familiar(four,five)
| ~ familiar(four,six)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_254,c_236]) ).
cnf(c_331,plain,
( familiar(four,five)
| ~ familiar(four,six)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1092]) ).
cnf(c_1093,plain,
( familiar(three,five)
| familiar(four,five)
| ~ familiar(four,six)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_257,c_237]) ).
cnf(c_342,plain,
( familiar(four,five)
| ~ familiar(four,six)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1093]) ).
cnf(c_1094,plain,
( familiar(one,five)
| familiar(three,five)
| ~ familiar(three,four)
| familiar(one,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_263,c_250]) ).
cnf(c_357,plain,
( familiar(three,five)
| ~ familiar(three,four)
| familiar(one,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1094]) ).
cnf(c_1095,plain,
( familiar(two,five)
| familiar(one,five)
| ~ familiar(two,four)
| familiar(one,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_263,c_246]) ).
cnf(c_359,plain,
( familiar(two,five)
| ~ familiar(two,four)
| familiar(one,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1095]) ).
cnf(c_1096,plain,
( familiar(three,five)
| familiar(two,five)
| ~ familiar(three,four)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_266,c_242]) ).
cnf(c_371,plain,
( familiar(three,five)
| ~ familiar(three,four)
| familiar(two,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1096]) ).
cnf(c_1097,plain,
( familiar(two,four)
| familiar(one,four)
| ~ familiar(two,three)
| familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_272,c_245]) ).
cnf(c_386,plain,
( familiar(two,four)
| ~ familiar(two,three)
| familiar(one,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1097]) ).
cnf(c_1098,plain,
( familiar(one,four)
| familiar(four,six)
| ~ familiar(three,six)
| familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_274,c_247]) ).
cnf(c_391,plain,
( familiar(four,six)
| ~ familiar(three,six)
| familiar(one,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1098]) ).
cnf(c_1099,plain,
( familiar(two,four)
| familiar(four,six)
| ~ familiar(three,six)
| familiar(two,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_277,c_248]) ).
cnf(c_401,plain,
( familiar(four,six)
| ~ familiar(three,six)
| familiar(two,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1099]) ).
cnf(c_1100,plain,
( familiar(two,five)
| familiar(one,five)
| ~ familiar(one,three)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_285,c_246]) ).
cnf(c_417,plain,
( familiar(one,five)
| ~ familiar(one,three)
| familiar(three,five)
| familiar(two,five) ),
inference(copy,[status(thm)],[c_1100]) ).
cnf(c_1101,plain,
( familiar(three,five)
| familiar(five,six)
| familiar(three,five)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_311,c_233]) ).
cnf(c_1102,plain,
( familiar(three,five)
| familiar(three,five)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1101]) ).
cnf(c_450,plain,
( familiar(three,five)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1102]) ).
cnf(c_456,plain,
( ~ familiar(A,five)
| ~ familiar(one,A)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_450,c_14]) ).
cnf(c_1103,plain,
( familiar(two,five)
| familiar(five,six)
| familiar(two,five)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_312,c_232]) ).
cnf(c_1104,plain,
( familiar(two,five)
| familiar(two,five)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1103]) ).
cnf(c_461,plain,
( familiar(two,five)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1104]) ).
cnf(c_466,plain,
( ~ familiar(A,five)
| ~ familiar(one,A)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_461,c_14]) ).
cnf(c_1105,plain,
( familiar(four,five)
| familiar(five,six)
| familiar(four,five)
| familiar(one,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_316,c_234]) ).
cnf(c_1106,plain,
( familiar(four,five)
| familiar(four,five)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1105]) ).
cnf(c_469,plain,
( familiar(four,five)
| familiar(one,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1106]) ).
cnf(c_478,plain,
( ~ familiar(A,five)
| ~ familiar(one,A)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_469,c_14]) ).
cnf(c_1107,plain,
( familiar(three,five)
| familiar(five,six)
| familiar(three,five)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_329,c_233]) ).
cnf(c_1108,plain,
( familiar(three,five)
| familiar(three,five)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1107]) ).
cnf(c_482,plain,
( familiar(three,five)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1108]) ).
cnf(c_484,plain,
( ~ familiar(A,five)
| ~ familiar(two,A)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_482,c_14]) ).
cnf(c_1109,plain,
( familiar(four,five)
| familiar(five,six)
| familiar(four,five)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_331,c_234]) ).
cnf(c_1110,plain,
( familiar(four,five)
| familiar(four,five)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1109]) ).
cnf(c_487,plain,
( familiar(four,five)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1110]) ).
cnf(c_492,plain,
( ~ familiar(A,five)
| ~ familiar(two,A)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_487,c_14]) ).
cnf(c_1111,plain,
( familiar(four,five)
| familiar(five,six)
| familiar(four,five)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_342,c_234]) ).
cnf(c_1112,plain,
( familiar(four,five)
| familiar(four,five)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1111]) ).
cnf(c_495,plain,
( familiar(four,five)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1112]) ).
cnf(c_1113,plain,
( familiar(three,five)
| familiar(four,five)
| familiar(three,five)
| familiar(one,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_357,c_237]) ).
cnf(c_1114,plain,
( familiar(three,five)
| familiar(three,five)
| familiar(one,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1113]) ).
cnf(c_499,plain,
( familiar(three,five)
| familiar(one,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1114]) ).
cnf(c_505,plain,
( ~ familiar(five,six)
| familiar(two,six)
| familiar(one,two)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_499,c_290]) ).
cnf(c_508,plain,
( ~ familiar(A,five)
| ~ familiar(one,A)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_499,c_14]) ).
cnf(c_1115,plain,
( familiar(two,five)
| familiar(four,five)
| familiar(two,five)
| familiar(one,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_359,c_236]) ).
cnf(c_1116,plain,
( familiar(two,five)
| familiar(two,five)
| familiar(one,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1115]) ).
cnf(c_511,plain,
( familiar(two,five)
| familiar(one,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1116]) ).
cnf(c_512,plain,
( ~ familiar(five,six)
| familiar(one,three)
| familiar(three,six)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_511,c_305]) ).
cnf(c_518,plain,
( ~ familiar(A,five)
| ~ familiar(one,A)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_511,c_14]) ).
cnf(c_1117,plain,
( familiar(three,five)
| familiar(four,five)
| familiar(three,five)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_371,c_237]) ).
cnf(c_1118,plain,
( familiar(three,five)
| familiar(three,five)
| familiar(two,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1117]) ).
cnf(c_521,plain,
( familiar(three,five)
| familiar(two,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1118]) ).
cnf(c_526,plain,
( ~ familiar(two,A)
| ~ familiar(five,A)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_521,c_14]) ).
cnf(c_1119,plain,
( familiar(two,four)
| familiar(three,four)
| familiar(two,four)
| familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_386,c_239]) ).
cnf(c_1120,plain,
( familiar(two,four)
| familiar(two,four)
| familiar(one,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1119]) ).
cnf(c_528,plain,
( familiar(two,four)
| familiar(one,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1120]) ).
cnf(c_1121,plain,
( familiar(four,six)
| familiar(three,four)
| familiar(four,six)
| familiar(one,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_391,c_240]) ).
cnf(c_1122,plain,
( familiar(four,six)
| familiar(four,six)
| familiar(one,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1121]) ).
cnf(c_537,plain,
( familiar(four,six)
| familiar(one,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1122]) ).
cnf(c_544,plain,
( ~ familiar(A,four)
| ~ familiar(one,A)
| familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_537,c_14]) ).
cnf(c_546,plain,
( ~ familiar(one,A)
| ~ familiar(four,A)
| familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_537,c_14]) ).
cnf(c_1123,plain,
( familiar(four,six)
| familiar(three,four)
| familiar(four,six)
| familiar(two,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_401,c_240]) ).
cnf(c_1124,plain,
( familiar(four,six)
| familiar(four,six)
| familiar(two,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1123]) ).
cnf(c_547,plain,
( familiar(four,six)
| familiar(two,four)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1124]) ).
cnf(c_1125,plain,
( familiar(one,five)
| familiar(three,five)
| familiar(one,five)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_417,c_250]) ).
cnf(c_1126,plain,
( familiar(one,five)
| familiar(one,five)
| familiar(three,five)
| familiar(two,five) ),
inference(copy,[status(thm)],[c_1125]) ).
cnf(c_563,plain,
( familiar(one,five)
| familiar(three,five)
| familiar(two,five) ),
inference(copy,[status(thm)],[c_1126]) ).
cnf(c_565,plain,
( ~ familiar(five,six)
| familiar(one,four)
| familiar(four,six)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_563,c_299]) ).
cnf(c_569,plain,
( ~ familiar(A,five)
| ~ familiar(one,A)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_563,c_14]) ).
cnf(c_1127,plain,
( familiar(three,five)
| familiar(five,six)
| ~ familiar(one,two)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_456,c_482]) ).
cnf(c_1128,plain,
( familiar(three,five)
| ~ familiar(one,two)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1127]) ).
cnf(c_586,plain,
( ~ familiar(one,two)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1128]) ).
cnf(c_587,plain,
( familiar(two,four)
| familiar(one,four)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_586,c_245]) ).
cnf(c_1129,plain,
( familiar(four,five)
| familiar(five,six)
| ~ familiar(one,three)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_478,c_495]) ).
cnf(c_1130,plain,
( familiar(four,five)
| ~ familiar(one,three)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1129]) ).
cnf(c_605,plain,
( ~ familiar(one,three)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1130]) ).
cnf(c_1131,plain,
( familiar(four,five)
| familiar(five,six)
| ~ familiar(one,two)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_478,c_487]) ).
cnf(c_1132,plain,
( familiar(four,five)
| ~ familiar(one,two)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1131]) ).
cnf(c_606,plain,
( ~ familiar(one,two)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1132]) ).
cnf(c_610,plain,
( familiar(one,three)
| familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_606,c_241]) ).
cnf(c_1133,plain,
( familiar(four,five)
| familiar(five,six)
| ~ familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_492,c_495]) ).
cnf(c_1134,plain,
( familiar(four,five)
| ~ familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1133]) ).
cnf(c_614,plain,
( ~ familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1134]) ).
cnf(c_1135,plain,
( familiar(three,five)
| familiar(four,five)
| ~ familiar(one,two)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_508,c_521]) ).
cnf(c_1136,plain,
( familiar(three,five)
| ~ familiar(one,two)
| familiar(three,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1135]) ).
cnf(c_624,plain,
( ~ familiar(one,two)
| familiar(three,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1136]) ).
cnf(c_1137,plain,
( familiar(four,six)
| familiar(three,four)
| ~ familiar(one,two)
| familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_544,c_547]) ).
cnf(c_1138,plain,
( familiar(four,six)
| ~ familiar(one,two)
| familiar(four,six)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1137]) ).
cnf(c_646,plain,
( ~ familiar(one,two)
| familiar(four,six)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1138]) ).
cnf(c_647,plain,
( familiar(two,five)
| familiar(one,five)
| familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_646,c_246]) ).
cnf(c_1139,plain,
( familiar(four,five)
| familiar(five,six)
| familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_610,c_605]) ).
cnf(c_1140,plain,
( familiar(four,five)
| familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1139]) ).
cnf(c_699,plain,
( familiar(two,three)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1140]) ).
cnf(c_1141,plain,
( familiar(four,five)
| familiar(five,six)
| familiar(four,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_699,c_614]) ).
cnf(c_1142,plain,
( familiar(four,five)
| familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1141]) ).
cnf(c_700,plain,
( familiar(four,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1142]) ).
cnf(c_1143,plain,
( ~ familiar(two,four)
| familiar(three,five)
| familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_700,c_484]) ).
cnf(c_701,plain,
( ~ familiar(two,four)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1143]) ).
cnf(c_1144,plain,
( ~ familiar(one,four)
| familiar(two,five)
| familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_700,c_466]) ).
cnf(c_702,plain,
( ~ familiar(one,four)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1144]) ).
cnf(c_1145,plain,
( ~ familiar(one,four)
| familiar(three,five)
| familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_700,c_456]) ).
cnf(c_703,plain,
( ~ familiar(one,four)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1145]) ).
cnf(c_705,plain,
( ~ familiar(A,five)
| ~ familiar(A,four)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_700,c_14]) ).
cnf(c_709,plain,
( familiar(four,six)
| familiar(three,four)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_702,c_537]) ).
cnf(c_710,plain,
( familiar(two,four)
| familiar(three,four)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_702,c_528]) ).
cnf(c_1146,plain,
( familiar(two,four)
| familiar(three,five)
| familiar(five,six)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_703,c_587]) ).
cnf(c_1147,plain,
( familiar(two,four)
| familiar(three,five)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1146]) ).
cnf(c_711,plain,
( familiar(two,four)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1147]) ).
cnf(c_716,plain,
( familiar(four,six)
| familiar(three,four)
| ~ familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_705,c_547]) ).
cnf(c_1148,plain,
( familiar(three,five)
| familiar(five,six)
| familiar(three,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_711,c_701]) ).
cnf(c_1149,plain,
( familiar(three,five)
| familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1148]) ).
cnf(c_720,plain,
( familiar(three,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1149]) ).
cnf(c_723,plain,
( ~ familiar(A,five)
| ~ familiar(three,A)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_720,c_14]) ).
cnf(c_724,plain,
( ~ familiar(A,five)
| ~ familiar(A,three)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_720,c_14]) ).
cnf(c_1150,plain,
( familiar(five,six)
| ~ familiar(three,four)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_723,c_700]) ).
cnf(c_729,plain,
( ~ familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1150]) ).
cnf(c_732,plain,
( familiar(two,four)
| familiar(three,four)
| ~ familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_724,c_239]) ).
cnf(c_1151,plain,
( ~ familiar(four,five)
| familiar(four,six)
| familiar(three,four)
| familiar(two,five)
| familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_647,c_546]) ).
cnf(c_1152,plain,
( ~ familiar(four,five)
| familiar(four,six)
| familiar(two,five)
| familiar(four,six)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1151]) ).
cnf(c_752,plain,
( ~ familiar(four,five)
| familiar(two,five)
| familiar(four,six)
| familiar(three,four) ),
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_1153,plain,
( familiar(four,six)
| familiar(three,four)
| familiar(five,six)
| familiar(four,six)
| familiar(three,four)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_716,c_709]) ).
cnf(c_1154,plain,
( familiar(four,six)
| familiar(three,four)
| familiar(four,six)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_1155,plain,
( familiar(four,six)
| familiar(four,six)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1154]) ).
cnf(c_780,plain,
( familiar(four,six)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1155]) ).
cnf(c_1156,plain,
( familiar(five,six)
| familiar(four,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_780,c_729]) ).
cnf(c_781,plain,
( familiar(four,six)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1156]) ).
cnf(c_1157,plain,
( ~ familiar(two,four)
| familiar(two,five)
| familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_781,c_254]) ).
cnf(c_790,plain,
( ~ familiar(two,four)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1157]) ).
cnf(c_1158,plain,
( familiar(three,four)
| familiar(two,five)
| familiar(five,six)
| familiar(two,five)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_790,c_710]) ).
cnf(c_1159,plain,
( familiar(three,four)
| familiar(two,five)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1158]) ).
cnf(c_796,plain,
( familiar(three,four)
| familiar(two,five)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1159]) ).
cnf(c_1160,plain,
( familiar(three,four)
| familiar(five,six)
| familiar(two,four)
| familiar(three,four)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_732,c_796]) ).
cnf(c_1161,plain,
( familiar(three,four)
| familiar(two,four)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1160]) ).
cnf(c_808,plain,
( familiar(two,four)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1161]) ).
cnf(c_1162,plain,
( ~ familiar(two,five)
| familiar(five,six)
| familiar(three,four)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_808,c_705]) ).
cnf(c_809,plain,
( ~ familiar(two,five)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1162]) ).
cnf(c_1163,plain,
( familiar(three,four)
| familiar(five,six)
| familiar(three,four)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_809,c_796]) ).
cnf(c_1164,plain,
( familiar(three,four)
| familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1163]) ).
cnf(c_814,plain,
( familiar(three,four)
| familiar(five,six) ),
inference(copy,[status(thm)],[c_1164]) ).
cnf(c_1165,plain,
( familiar(five,six)
| familiar(five,six) ),
inference(resolve,[status(thm)],[c_814,c_729]) ).
cnf(c_815,plain,
familiar(five,six),
inference(copy,[status(thm)],[c_1165]) ).
cnf(c_818,plain,
( familiar(one,four)
| familiar(four,six)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_815,c_565]) ).
cnf(c_824,plain,
( familiar(one,three)
| familiar(three,six)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_815,c_512]) ).
cnf(c_825,plain,
( familiar(two,six)
| familiar(one,two)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_815,c_505]) ).
cnf(c_831,plain,
( ~ familiar(two,five)
| familiar(two,four)
| familiar(four,six) ),
inference(resolve,[status(thm)],[c_815,c_302]) ).
cnf(c_837,plain,
( ~ familiar(two,five)
| familiar(three,six)
| familiar(two,three) ),
inference(resolve,[status(thm)],[c_815,c_287]) ).
cnf(c_841,plain,
( ~ familiar(A,six)
| ~ familiar(A,five) ),
inference(resolve,[status(thm)],[c_815,c_14]) ).
cnf(c_1166,plain,
( ~ familiar(four,five)
| familiar(three,five)
| familiar(two,five)
| familiar(four,six)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_818,c_569]) ).
cnf(c_1167,plain,
( ~ familiar(four,five)
| familiar(three,five)
| familiar(four,six)
| familiar(three,five)
| familiar(two,five) ),
inference(copy,[status(thm)],[c_1166]) ).
cnf(c_853,plain,
( ~ familiar(four,five)
| familiar(four,six)
| familiar(three,five)
| familiar(two,five) ),
inference(copy,[status(thm)],[c_1167]) ).
cnf(c_1168,plain,
( familiar(three,five)
| familiar(four,five)
| familiar(two,six)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_825,c_624]) ).
cnf(c_1169,plain,
( familiar(three,five)
| familiar(two,six)
| familiar(three,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1168]) ).
cnf(c_900,plain,
( familiar(two,six)
| familiar(three,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1169]) ).
cnf(c_1170,plain,
( ~ familiar(five,six)
| familiar(three,five)
| familiar(four,five)
| familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_900,c_526]) ).
cnf(c_1171,plain,
( ~ familiar(five,six)
| familiar(three,five)
| familiar(three,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1170]) ).
cnf(c_1172,plain,
( ~ familiar(five,six)
| familiar(three,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1171]) ).
cnf(c_903,plain,
( familiar(three,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_815,c_1172]) ).
cnf(c_1173,plain,
( ~ familiar(one,three)
| familiar(two,five)
| familiar(four,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_903,c_518]) ).
cnf(c_905,plain,
( ~ familiar(one,three)
| familiar(two,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1173]) ).
cnf(c_907,plain,
( ~ familiar(A,five)
| ~ familiar(A,three)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_903,c_14]) ).
cnf(c_908,plain,
( ~ familiar(three,A)
| ~ familiar(five,A)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_903,c_14]) ).
cnf(c_1174,plain,
( familiar(three,six)
| familiar(two,five)
| familiar(four,five)
| familiar(two,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_905,c_824]) ).
cnf(c_1175,plain,
( familiar(three,six)
| familiar(two,five)
| familiar(two,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1174]) ).
cnf(c_915,plain,
( familiar(three,six)
| familiar(two,five)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1175]) ).
cnf(c_1176,plain,
( familiar(three,six)
| familiar(two,three)
| familiar(three,six)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_915,c_837]) ).
cnf(c_923,plain,
( familiar(two,three)
| familiar(three,six)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1176]) ).
cnf(c_1177,plain,
( ~ familiar(two,five)
| familiar(four,five)
| familiar(three,six)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_923,c_907]) ).
cnf(c_930,plain,
( ~ familiar(two,five)
| familiar(three,six)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1177]) ).
cnf(c_1178,plain,
( familiar(three,six)
| familiar(four,five)
| familiar(three,six)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_930,c_915]) ).
cnf(c_1179,plain,
( familiar(three,six)
| familiar(three,six)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1178]) ).
cnf(c_935,plain,
( familiar(three,six)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1179]) ).
cnf(c_1180,plain,
( ~ familiar(five,six)
| familiar(four,five)
| familiar(four,five) ),
inference(resolve,[status(thm)],[c_935,c_908]) ).
cnf(c_1181,plain,
( ~ familiar(five,six)
| familiar(four,five) ),
inference(copy,[status(thm)],[c_1180]) ).
cnf(c_936,plain,
familiar(four,five),
inference(resolve,[status(thm)],[c_815,c_1181]) ).
cnf(c_937,plain,
( familiar(four,six)
| familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_936,c_853]) ).
cnf(c_938,plain,
( familiar(two,five)
| familiar(four,six)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_936,c_752]) ).
cnf(c_942,plain,
( ~ familiar(A,five)
| ~ familiar(A,four) ),
inference(resolve,[status(thm)],[c_936,c_14]) ).
cnf(c_944,plain,
~ familiar(four,six),
inference(resolve,[status(thm)],[c_841,c_936]) ).
cnf(c_945,plain,
( familiar(two,five)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_944,c_938]) ).
cnf(c_946,plain,
( familiar(three,five)
| familiar(two,five) ),
inference(resolve,[status(thm)],[c_944,c_937]) ).
cnf(c_953,plain,
( ~ familiar(two,five)
| familiar(two,four) ),
inference(resolve,[status(thm)],[c_944,c_831]) ).
cnf(c_978,plain,
( familiar(two,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_944,c_547]) ).
cnf(c_1027,plain,
( familiar(three,five)
| familiar(two,four) ),
inference(resolve,[status(thm)],[c_953,c_946]) ).
cnf(c_1029,plain,
( ~ familiar(two,five)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_978,c_942]) ).
cnf(c_1034,plain,
( ~ familiar(two,five)
| familiar(three,five) ),
inference(resolve,[status(thm)],[c_1027,c_942]) ).
cnf(c_1182,plain,
( familiar(three,four)
| familiar(three,four) ),
inference(resolve,[status(thm)],[c_1029,c_945]) ).
cnf(c_1039,plain,
familiar(three,four),
inference(copy,[status(thm)],[c_1182]) ).
cnf(c_1041,plain,
~ familiar(three,five),
inference(resolve,[status(thm)],[c_1039,c_942]) ).
cnf(c_1048,plain,
~ familiar(two,five),
inference(resolve,[status(thm)],[c_1041,c_1034]) ).
cnf(c_1183,plain,
familiar(three,five),
inference(resolve,[status(thm)],[c_1048,c_946]) ).
cnf(c_1057,plain,
$false,
inference(resolve,[status(thm)],[c_1041,c_1183]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ028-5 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 05:07:51 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 3780388 was started by sandbox2 on n018,
% 0.08/0.37 % Sat Sep 26 05:07:51 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 0.13/0.48
% 0.13/0.48 % given #500 (A,wt=15): 392 familiar(three,four) | familiar(one,four) | -familiar(three,two) | familiar(one,five) | familiar(two,five). [resolve(274,d,246,a)].
% 0.13/0.48
% 0.13/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.13/0.48
% 0.13/0.48 % Proof 1 at 0.07 (+ 0.03) seconds.
% 0.13/0.48 % Length of proof is 213.
% 0.13/0.48 % Level of proof is 44.
% 0.13/0.48 % Maximum clause weight is 15.000.
% 0.13/0.48 % Given clauses 596.
% 0.13/0.48
% 0.13/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------