%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ028-5 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:37:38 EDT 2024
% Result : Unsatisfiable 61.72s 61.91s
% Output : Refutation 61.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 15
% Syntax : Number of clauses : 263 ( 31 unt; 179 nHn; 263 RR)
% Number of literals : 699 ( 0 equ; 205 neg)
% Maximal clause size : 5 ( 2 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 : 55 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(person1,axiom,
person(one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person1) ).
cnf(person2,axiom,
person(two),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person2) ).
cnf(order1,axiom,
after(one,two),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order1) ).
cnf(familiar_or_not,axiom,
( familiar(X9,X8)
| not_familiar(X9,X8)
| ~ person(X9)
| ~ person(X8)
| ~ after(X9,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',familiar_or_not) ).
cnf(c14,plain,
( familiar(one,two)
| not_familiar(one,two)
| ~ person(one)
| ~ person(two) ),
inference(resolution,[status(thm)],[familiar_or_not,order1]) ).
cnf(c67,plain,
( familiar(one,two)
| not_familiar(one,two)
| ~ person(one) ),
inference(resolution,[status(thm)],[c14,person2]) ).
cnf(c84,plain,
( familiar(one,two)
| not_familiar(one,two) ),
inference(resolution,[status(thm)],[c67,person1]) ).
cnf(person3,axiom,
person(three),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person3) ).
cnf(order2,axiom,
after(two,three),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order2) ).
cnf(c11,plain,
( familiar(two,three)
| not_familiar(two,three)
| ~ person(two)
| ~ person(three) ),
inference(resolution,[status(thm)],[familiar_or_not,order2]) ).
cnf(c52,plain,
( familiar(two,three)
| not_familiar(two,three)
| ~ person(two) ),
inference(resolution,[status(thm)],[c11,person3]) ).
cnf(c64,plain,
( familiar(two,three)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c52,person2]) ).
cnf(three_familiar,negated_conjecture,
( ~ familiar(X12,X13)
| ~ familiar(X13,X14)
| ~ familiar(X12,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',three_familiar) ).
cnf(transitivity_of_order,axiom,
( after(X4,X3)
| ~ after(X4,X2)
| ~ after(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_order) ).
cnf(c1,plain,
( after(X6,three)
| ~ after(X6,two) ),
inference(resolution,[status(thm)],[transitivity_of_order,order2]) ).
cnf(c6,plain,
after(one,three),
inference(resolution,[status(thm)],[c1,order1]) ).
cnf(c10,plain,
( familiar(one,three)
| not_familiar(one,three)
| ~ person(one)
| ~ person(three) ),
inference(resolution,[status(thm)],[familiar_or_not,c6]) ).
cnf(c49,plain,
( familiar(one,three)
| not_familiar(one,three)
| ~ person(one) ),
inference(resolution,[status(thm)],[c10,person3]) ).
cnf(c61,plain,
( familiar(one,three)
| not_familiar(one,three) ),
inference(resolution,[status(thm)],[c49,person1]) ).
cnf(c62,plain,
( not_familiar(one,three)
| ~ familiar(one,X39)
| ~ familiar(X39,three) ),
inference(resolution,[status(thm)],[c61,three_familiar]) ).
cnf(c75,plain,
( not_familiar(one,three)
| ~ familiar(one,two)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c62,c64]) ).
cnf(c152,plain,
( not_familiar(one,three)
| not_familiar(two,three)
| not_familiar(one,two) ),
inference(resolution,[status(thm)],[c75,c84]) ).
cnf(person4,axiom,
person(four),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person4) ).
cnf(order3,axiom,
after(three,four),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order3) ).
cnf(c15,plain,
( familiar(three,four)
| not_familiar(three,four)
| ~ person(three)
| ~ person(four) ),
inference(resolution,[status(thm)],[familiar_or_not,order3]) ).
cnf(c76,plain,
( familiar(three,four)
| not_familiar(three,four)
| ~ person(three) ),
inference(resolution,[status(thm)],[c15,person4]) ).
cnf(c97,plain,
( familiar(three,four)
| not_familiar(three,four) ),
inference(resolution,[status(thm)],[c76,person3]) ).
cnf(c4,plain,
( after(X11,four)
| ~ after(X11,three) ),
inference(resolution,[status(thm)],[transitivity_of_order,order3]) ).
cnf(c18,plain,
after(two,four),
inference(resolution,[status(thm)],[c4,order2]) ).
cnf(c23,plain,
( familiar(two,four)
| not_familiar(two,four)
| ~ person(two)
| ~ person(four) ),
inference(resolution,[status(thm)],[c18,familiar_or_not]) ).
cnf(c94,plain,
( familiar(two,four)
| not_familiar(two,four)
| ~ person(two) ),
inference(resolution,[status(thm)],[c23,person4]) ).
cnf(c110,plain,
( familiar(two,four)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c94,person2]) ).
cnf(c111,plain,
( not_familiar(two,four)
| ~ familiar(two,X55)
| ~ familiar(X55,four) ),
inference(resolution,[status(thm)],[c110,three_familiar]) ).
cnf(c145,plain,
( not_familiar(two,four)
| ~ familiar(two,three)
| not_familiar(three,four) ),
inference(resolution,[status(thm)],[c111,c97]) ).
cnf(c235,plain,
( not_familiar(two,four)
| not_familiar(three,four)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c145,c64]) ).
cnf(three_not_familiar,negated_conjecture,
( ~ not_familiar(X21,X22)
| ~ not_familiar(X22,X23)
| ~ not_familiar(X21,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',three_not_familiar) ).
cnf(c17,plain,
after(one,four),
inference(resolution,[status(thm)],[c4,c6]) ).
cnf(c20,plain,
( familiar(one,four)
| not_familiar(one,four)
| ~ person(one)
| ~ person(four) ),
inference(resolution,[status(thm)],[c17,familiar_or_not]) ).
cnf(c89,plain,
( familiar(one,four)
| not_familiar(one,four)
| ~ person(one) ),
inference(resolution,[status(thm)],[c20,person4]) ).
cnf(c107,plain,
( familiar(one,four)
| not_familiar(one,four) ),
inference(resolution,[status(thm)],[c89,person1]) ).
cnf(c108,plain,
( not_familiar(one,four)
| ~ familiar(one,X53)
| ~ familiar(X53,four) ),
inference(resolution,[status(thm)],[c107,three_familiar]) ).
cnf(c140,plain,
( not_familiar(one,four)
| ~ familiar(one,two)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c108,c110]) ).
cnf(c232,plain,
( not_familiar(one,four)
| not_familiar(two,four)
| not_familiar(one,two) ),
inference(resolution,[status(thm)],[c140,c84]) ).
cnf(c357,plain,
( not_familiar(two,four)
| not_familiar(one,two)
| ~ not_familiar(one,X84)
| ~ not_familiar(X84,four) ),
inference(resolution,[status(thm)],[c232,three_not_familiar]) ).
cnf(c1284,plain,
( not_familiar(two,four)
| not_familiar(one,two)
| ~ not_familiar(one,three)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c357,c235]) ).
cnf(c15576,plain,
( not_familiar(two,four)
| not_familiar(one,two)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c1284,c152]) ).
cnf(person5,axiom,
person(five),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person5) ).
cnf(order4,axiom,
after(four,five),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order4) ).
cnf(c12,plain,
( familiar(four,five)
| not_familiar(four,five)
| ~ person(four)
| ~ person(five) ),
inference(resolution,[status(thm)],[familiar_or_not,order4]) ).
cnf(c56,plain,
( familiar(four,five)
| not_familiar(four,five)
| ~ person(four) ),
inference(resolution,[status(thm)],[c12,person5]) ).
cnf(c68,plain,
( familiar(four,five)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c56,person4]) ).
cnf(c2,plain,
( after(X7,five)
| ~ after(X7,four) ),
inference(resolution,[status(thm)],[transitivity_of_order,order4]) ).
cnf(c24,plain,
after(two,five),
inference(resolution,[status(thm)],[c18,c2]) ).
cnf(c30,plain,
( familiar(two,five)
| not_familiar(two,five)
| ~ person(two)
| ~ person(five) ),
inference(resolution,[status(thm)],[c24,familiar_or_not]) ).
cnf(c106,plain,
( familiar(two,five)
| not_familiar(two,five)
| ~ person(two) ),
inference(resolution,[status(thm)],[c30,person5]) ).
cnf(c130,plain,
( familiar(two,five)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c106,person2]) ).
cnf(c132,plain,
( not_familiar(two,five)
| ~ familiar(two,X59)
| ~ familiar(X59,five) ),
inference(resolution,[status(thm)],[c130,three_familiar]) ).
cnf(c176,plain,
( not_familiar(two,five)
| ~ familiar(two,four)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c132,c68]) ).
cnf(c271,plain,
( not_familiar(two,five)
| not_familiar(four,five)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c176,c110]) ).
cnf(c8,plain,
after(three,five),
inference(resolution,[status(thm)],[c2,order3]) ).
cnf(c13,plain,
( familiar(three,five)
| not_familiar(three,five)
| ~ person(three)
| ~ person(five) ),
inference(resolution,[status(thm)],[familiar_or_not,c8]) ).
cnf(c60,plain,
( familiar(three,five)
| not_familiar(three,five)
| ~ person(three) ),
inference(resolution,[status(thm)],[c13,person5]) ).
cnf(c71,plain,
( familiar(three,five)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c60,person3]) ).
cnf(c179,plain,
( not_familiar(two,five)
| ~ familiar(two,three)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c132,c71]) ).
cnf(c272,plain,
( not_familiar(two,five)
| not_familiar(three,five)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c179,c64]) ).
cnf(c586,plain,
( not_familiar(two,five)
| not_familiar(two,three)
| ~ not_familiar(three,X121)
| ~ not_familiar(X121,five) ),
inference(resolution,[status(thm)],[c272,three_not_familiar]) ).
cnf(c2378,plain,
( not_familiar(two,five)
| not_familiar(two,three)
| ~ not_familiar(three,four)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c586,c271]) ).
cnf(c35658,plain,
( not_familiar(two,five)
| not_familiar(two,three)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c2378,c235]) ).
cnf(c21,plain,
after(one,five),
inference(resolution,[status(thm)],[c17,c2]) ).
cnf(c26,plain,
( familiar(one,five)
| not_familiar(one,five)
| ~ person(one)
| ~ person(five) ),
inference(resolution,[status(thm)],[c21,familiar_or_not]) ).
cnf(c101,plain,
( familiar(one,five)
| not_familiar(one,five)
| ~ person(one) ),
inference(resolution,[status(thm)],[c26,person5]) ).
cnf(c120,plain,
( familiar(one,five)
| not_familiar(one,five) ),
inference(resolution,[status(thm)],[c101,person1]) ).
cnf(c121,plain,
( not_familiar(one,five)
| ~ familiar(one,X57)
| ~ familiar(X57,five) ),
inference(resolution,[status(thm)],[c120,three_familiar]) ).
cnf(c158,plain,
( not_familiar(one,five)
| ~ familiar(one,two)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c121,c130]) ).
cnf(c160,plain,
( not_familiar(one,five)
| ~ familiar(one,three)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c121,c71]) ).
cnf(c63,plain,
( familiar(one,three)
| ~ not_familiar(one,X40)
| ~ not_familiar(X40,three) ),
inference(resolution,[status(thm)],[c61,three_not_familiar]) ).
cnf(c77,plain,
( familiar(one,three)
| ~ not_familiar(one,two)
| familiar(two,three) ),
inference(resolution,[status(thm)],[c63,c64]) ).
cnf(c165,plain,
( familiar(one,three)
| familiar(two,three)
| familiar(one,two) ),
inference(resolution,[status(thm)],[c77,c84]) ).
cnf(c260,plain,
( familiar(two,three)
| familiar(one,two)
| not_familiar(one,five)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c165,c160]) ).
cnf(c1562,plain,
( familiar(one,two)
| not_familiar(one,five)
| not_familiar(three,five)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c260,c179]) ).
cnf(c17814,plain,
( not_familiar(one,five)
| not_familiar(three,five)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c1562,c158]) ).
cnf(c17970,plain,
( not_familiar(one,five)
| not_familiar(three,five)
| ~ not_familiar(two,X226)
| ~ not_familiar(X226,five) ),
inference(resolution,[status(thm)],[c17814,three_not_familiar]) ).
cnf(c251,plain,
( not_familiar(one,five)
| not_familiar(three,five)
| not_familiar(one,three) ),
inference(resolution,[status(thm)],[c160,c61]) ).
cnf(c72,plain,
( not_familiar(three,five)
| ~ familiar(three,X45)
| ~ familiar(X45,five) ),
inference(resolution,[status(thm)],[c71,three_familiar]) ).
cnf(c92,plain,
( not_familiar(three,five)
| ~ familiar(three,four)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c72,c68]) ).
cnf(c229,plain,
( not_familiar(three,five)
| not_familiar(four,five)
| not_familiar(three,four) ),
inference(resolution,[status(thm)],[c92,c97]) ).
cnf(c157,plain,
( not_familiar(one,five)
| ~ familiar(one,four)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c121,c68]) ).
cnf(c249,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| not_familiar(one,four) ),
inference(resolution,[status(thm)],[c157,c107]) ).
cnf(c459,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| ~ not_familiar(one,X101)
| ~ not_familiar(X101,four) ),
inference(resolution,[status(thm)],[c249,three_not_familiar]) ).
cnf(c1705,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| ~ not_familiar(one,three)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c459,c229]) ).
cnf(c19239,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c1705,c251]) ).
cnf(c19288,plain,
( not_familiar(one,five)
| not_familiar(three,five)
| ~ not_familiar(two,four) ),
inference(resolution,[status(thm)],[c19239,c17970]) ).
cnf(c19354,plain,
( not_familiar(one,five)
| not_familiar(three,five)
| familiar(two,four) ),
inference(resolution,[status(thm)],[c19288,c110]) ).
cnf(c17945,plain,
( not_familiar(one,five)
| not_familiar(two,five)
| ~ not_familiar(three,X225)
| ~ not_familiar(X225,five) ),
inference(resolution,[status(thm)],[c17814,three_not_familiar]) ).
cnf(c250,plain,
( not_familiar(one,five)
| not_familiar(two,five)
| not_familiar(one,two) ),
inference(resolution,[status(thm)],[c158,c84]) ).
cnf(c1712,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| ~ not_familiar(one,two)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c459,c271]) ).
cnf(c20016,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c1712,c250]) ).
cnf(c20087,plain,
( not_familiar(one,five)
| not_familiar(two,five)
| ~ not_familiar(three,four) ),
inference(resolution,[status(thm)],[c20016,c17945]) ).
cnf(c20139,plain,
( not_familiar(one,five)
| not_familiar(two,five)
| familiar(three,four) ),
inference(resolution,[status(thm)],[c20087,c97]) ).
cnf(person6,axiom,
person(six),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person6) ).
cnf(order5,axiom,
after(five,six),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order5) ).
cnf(c5,plain,
( after(X20,six)
| ~ after(X20,five) ),
inference(resolution,[status(thm)],[transitivity_of_order,order5]) ).
cnf(c33,plain,
after(four,six),
inference(resolution,[status(thm)],[c5,order4]) ).
cnf(c41,plain,
( familiar(four,six)
| not_familiar(four,six)
| ~ person(four)
| ~ person(six) ),
inference(resolution,[status(thm)],[c33,familiar_or_not]) ).
cnf(c127,plain,
( familiar(four,six)
| not_familiar(four,six)
| ~ person(four) ),
inference(resolution,[status(thm)],[c41,person6]) ).
cnf(c166,plain,
( familiar(four,six)
| not_familiar(four,six) ),
inference(resolution,[status(thm)],[c127,person4]) ).
cnf(c169,plain,
( familiar(four,six)
| ~ not_familiar(four,X64)
| ~ not_familiar(X64,six) ),
inference(resolution,[status(thm)],[c166,three_not_familiar]) ).
cnf(c16,plain,
( familiar(five,six)
| not_familiar(five,six)
| ~ person(five)
| ~ person(six) ),
inference(resolution,[status(thm)],[familiar_or_not,order5]) ).
cnf(c81,plain,
( familiar(five,six)
| not_familiar(five,six)
| ~ person(five) ),
inference(resolution,[status(thm)],[c16,person6]) ).
cnf(c100,plain,
( familiar(five,six)
| not_familiar(five,six) ),
inference(resolution,[status(thm)],[c81,person5]) ).
cnf(c34,plain,
after(two,six),
inference(resolution,[status(thm)],[c5,c24]) ).
cnf(c43,plain,
( familiar(two,six)
| not_familiar(two,six)
| ~ person(two)
| ~ person(six) ),
inference(resolution,[status(thm)],[c34,familiar_or_not]) ).
cnf(c131,plain,
( familiar(two,six)
| not_familiar(two,six)
| ~ person(two) ),
inference(resolution,[status(thm)],[c43,person6]) ).
cnf(c171,plain,
( familiar(two,six)
| not_familiar(two,six) ),
inference(resolution,[status(thm)],[c131,person2]) ).
cnf(c172,plain,
( not_familiar(two,six)
| ~ familiar(two,X65)
| ~ familiar(X65,six) ),
inference(resolution,[status(thm)],[c171,three_familiar]) ).
cnf(c209,plain,
( not_familiar(two,six)
| ~ familiar(two,five)
| not_familiar(five,six) ),
inference(resolution,[status(thm)],[c172,c100]) ).
cnf(c291,plain,
( not_familiar(two,six)
| not_familiar(five,six)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c209,c130]) ).
cnf(c32,plain,
after(one,six),
inference(resolution,[status(thm)],[c5,c21]) ).
cnf(c39,plain,
( familiar(one,six)
| not_familiar(one,six)
| ~ person(one)
| ~ person(six) ),
inference(resolution,[status(thm)],[c32,familiar_or_not]) ).
cnf(c116,plain,
( familiar(one,six)
| not_familiar(one,six)
| ~ person(one) ),
inference(resolution,[status(thm)],[c39,person6]) ).
cnf(c151,plain,
( familiar(one,six)
| not_familiar(one,six) ),
inference(resolution,[status(thm)],[c116,person1]) ).
cnf(c153,plain,
( not_familiar(one,six)
| ~ familiar(one,X61)
| ~ familiar(X61,six) ),
inference(resolution,[status(thm)],[c151,three_familiar]) ).
cnf(c189,plain,
( not_familiar(one,six)
| ~ familiar(one,five)
| not_familiar(five,six) ),
inference(resolution,[status(thm)],[c153,c100]) ).
cnf(c277,plain,
( not_familiar(one,six)
| not_familiar(five,six)
| not_familiar(one,five) ),
inference(resolution,[status(thm)],[c189,c120]) ).
cnf(c636,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(one,X129)
| ~ not_familiar(X129,six) ),
inference(resolution,[status(thm)],[c277,three_not_familiar]) ).
cnf(c2673,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(one,two)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c636,c291]) ).
cnf(c42002,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c2673,c250]) ).
cnf(c42123,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(two,X389)
| ~ not_familiar(X389,five) ),
inference(resolution,[status(thm)],[c42002,three_not_familiar]) ).
cnf(c35,plain,
after(three,six),
inference(resolution,[status(thm)],[c5,c8]) ).
cnf(c45,plain,
( familiar(three,six)
| not_familiar(three,six)
| ~ person(three)
| ~ person(six) ),
inference(resolution,[status(thm)],[c35,familiar_or_not]) ).
cnf(c144,plain,
( familiar(three,six)
| not_familiar(three,six)
| ~ person(three) ),
inference(resolution,[status(thm)],[c45,person6]) ).
cnf(c184,plain,
( familiar(three,six)
| not_familiar(three,six) ),
inference(resolution,[status(thm)],[c144,person3]) ).
cnf(c185,plain,
( not_familiar(three,six)
| ~ familiar(three,X67)
| ~ familiar(X67,six) ),
inference(resolution,[status(thm)],[c184,three_familiar]) ).
cnf(c219,plain,
( not_familiar(three,six)
| ~ familiar(three,five)
| not_familiar(five,six) ),
inference(resolution,[status(thm)],[c185,c100]) ).
cnf(c299,plain,
( not_familiar(three,six)
| not_familiar(five,six)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c219,c71]) ).
cnf(c2677,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(one,three)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c636,c299]) ).
cnf(c43643,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| not_familiar(three,five) ),
inference(resolution,[status(thm)],[c2677,c251]) ).
cnf(c43821,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(two,three) ),
inference(resolution,[status(thm)],[c43643,c42123]) ).
cnf(c43852,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| familiar(two,three) ),
inference(resolution,[status(thm)],[c43821,c64]) ).
cnf(c167,plain,
( not_familiar(four,six)
| ~ familiar(four,X63)
| ~ familiar(X63,six) ),
inference(resolution,[status(thm)],[c166,three_familiar]) ).
cnf(c199,plain,
( not_familiar(four,six)
| ~ familiar(four,five)
| not_familiar(five,six) ),
inference(resolution,[status(thm)],[c167,c100]) ).
cnf(c289,plain,
( not_familiar(four,six)
| not_familiar(five,six)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c199,c68]) ).
cnf(c2676,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(one,four)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c636,c289]) ).
cnf(c42532,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c2676,c249]) ).
cnf(c42704,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(two,four) ),
inference(resolution,[status(thm)],[c42532,c42123]) ).
cnf(c42740,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| familiar(two,four) ),
inference(resolution,[status(thm)],[c42704,c110]) ).
cnf(c42885,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ familiar(two,X395)
| ~ familiar(X395,four) ),
inference(resolution,[status(thm)],[c42740,three_familiar]) ).
cnf(c43767,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(three,X398)
| ~ not_familiar(X398,five) ),
inference(resolution,[status(thm)],[c43643,three_not_familiar]) ).
cnf(c44258,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ not_familiar(three,four) ),
inference(resolution,[status(thm)],[c43767,c42532]) ).
cnf(c44377,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| familiar(three,four) ),
inference(resolution,[status(thm)],[c44258,c97]) ).
cnf(c44544,plain,
( not_familiar(five,six)
| not_familiar(one,five)
| ~ familiar(two,three) ),
inference(resolution,[status(thm)],[c44377,c42885]) ).
cnf(c44574,plain,
( not_familiar(five,six)
| not_familiar(one,five) ),
inference(resolution,[status(thm)],[c44544,c43852]) ).
cnf(c44615,plain,
( not_familiar(one,five)
| familiar(four,six)
| ~ not_familiar(four,five) ),
inference(resolution,[status(thm)],[c44574,c169]) ).
cnf(c44968,plain,
( not_familiar(one,five)
| familiar(four,six)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c44615,c20016]) ).
cnf(c187,plain,
( familiar(three,six)
| ~ not_familiar(three,X68)
| ~ not_familiar(X68,six) ),
inference(resolution,[status(thm)],[c184,three_not_familiar]) ).
cnf(c44614,plain,
( not_familiar(one,five)
| familiar(three,six)
| ~ not_familiar(three,five) ),
inference(resolution,[status(thm)],[c44574,c187]) ).
cnf(c44928,plain,
( not_familiar(one,five)
| familiar(three,six)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c44614,c17814]) ).
cnf(c45434,plain,
( not_familiar(one,five)
| not_familiar(two,five)
| ~ familiar(three,X413)
| ~ familiar(X413,six) ),
inference(resolution,[status(thm)],[c44928,three_familiar]) ).
cnf(c51229,plain,
( not_familiar(one,five)
| not_familiar(two,five)
| ~ familiar(three,four) ),
inference(resolution,[status(thm)],[c45434,c44968]) ).
cnf(c51563,plain,
( not_familiar(one,five)
| not_familiar(two,five) ),
inference(resolution,[status(thm)],[c51229,c20139]) ).
cnf(c51634,plain,
( not_familiar(one,five)
| ~ not_familiar(two,X415)
| ~ not_familiar(X415,five) ),
inference(resolution,[status(thm)],[c51563,three_not_familiar]) ).
cnf(c52003,plain,
( not_familiar(one,five)
| ~ not_familiar(two,three)
| familiar(two,four) ),
inference(resolution,[status(thm)],[c51634,c19354]) ).
cnf(c174,plain,
( familiar(two,six)
| ~ not_familiar(two,X66)
| ~ not_familiar(X66,six) ),
inference(resolution,[status(thm)],[c171,three_not_familiar]) ).
cnf(c44622,plain,
( not_familiar(one,five)
| familiar(two,six)
| ~ not_familiar(two,five) ),
inference(resolution,[status(thm)],[c44574,c174]) ).
cnf(c51650,plain,
( not_familiar(one,five)
| familiar(two,six) ),
inference(resolution,[status(thm)],[c51563,c44622]) ).
cnf(c51785,plain,
( not_familiar(one,five)
| ~ familiar(two,X417)
| ~ familiar(X417,six) ),
inference(resolution,[status(thm)],[c51650,three_familiar]) ).
cnf(c44937,plain,
( not_familiar(one,five)
| familiar(three,six)
| familiar(two,four) ),
inference(resolution,[status(thm)],[c44614,c19354]) ).
cnf(c44939,plain,
( not_familiar(one,five)
| familiar(three,six)
| not_familiar(four,five) ),
inference(resolution,[status(thm)],[c44614,c19239]) ).
cnf(c45879,plain,
( not_familiar(one,five)
| familiar(three,six)
| familiar(four,six) ),
inference(resolution,[status(thm)],[c44939,c44615]) ).
cnf(c52135,plain,
( not_familiar(one,five)
| ~ familiar(two,four)
| familiar(three,six) ),
inference(resolution,[status(thm)],[c51785,c45879]) ).
cnf(c53899,plain,
( not_familiar(one,five)
| familiar(three,six) ),
inference(resolution,[status(thm)],[c52135,c44937]) ).
cnf(c53976,plain,
( not_familiar(one,five)
| ~ familiar(two,three) ),
inference(resolution,[status(thm)],[c53899,c51785]) ).
cnf(c54002,plain,
( not_familiar(one,five)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c53976,c64]) ).
cnf(c54132,plain,
( not_familiar(one,five)
| familiar(two,four) ),
inference(resolution,[status(thm)],[c54002,c52003]) ).
cnf(c20106,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| ~ not_familiar(two,X244)
| ~ not_familiar(X244,five) ),
inference(resolution,[status(thm)],[c20016,three_not_familiar]) ).
cnf(c20525,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| ~ not_familiar(two,three) ),
inference(resolution,[status(thm)],[c20106,c19239]) ).
cnf(c20558,plain,
( not_familiar(one,five)
| not_familiar(four,five)
| familiar(two,three) ),
inference(resolution,[status(thm)],[c20525,c64]) ).
cnf(c44971,plain,
( not_familiar(one,five)
| familiar(four,six)
| familiar(two,three) ),
inference(resolution,[status(thm)],[c44615,c20558]) ).
cnf(c54013,plain,
( not_familiar(one,five)
| familiar(four,six) ),
inference(resolution,[status(thm)],[c53976,c44971]) ).
cnf(c54315,plain,
( not_familiar(one,five)
| ~ familiar(two,four) ),
inference(resolution,[status(thm)],[c54013,c51785]) ).
cnf(c54718,plain,
not_familiar(one,five),
inference(resolution,[status(thm)],[c54315,c54132]) ).
cnf(c54749,plain,
( ~ not_familiar(one,X420)
| ~ not_familiar(X420,five) ),
inference(resolution,[status(thm)],[c54718,three_not_familiar]) ).
cnf(c54869,plain,
( ~ not_familiar(one,two)
| not_familiar(two,three)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c54749,c35658]) ).
cnf(c58871,plain,
( not_familiar(two,three)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c54869,c15576]) ).
cnf(c54865,plain,
( ~ not_familiar(one,two)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c54749,c130]) ).
cnf(c54968,plain,
( familiar(two,five)
| familiar(one,two) ),
inference(resolution,[status(thm)],[c54865,c84]) ).
cnf(c215,plain,
( familiar(two,six)
| ~ not_familiar(two,five)
| familiar(five,six) ),
inference(resolution,[status(thm)],[c174,c100]) ).
cnf(c296,plain,
( familiar(two,six)
| familiar(five,six)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c215,c130]) ).
cnf(c155,plain,
( familiar(one,six)
| ~ not_familiar(one,X62)
| ~ not_familiar(X62,six) ),
inference(resolution,[status(thm)],[c151,three_not_familiar]) ).
cnf(c195,plain,
( familiar(one,six)
| ~ not_familiar(one,five)
| familiar(five,six) ),
inference(resolution,[status(thm)],[c155,c100]) ).
cnf(c54753,plain,
( familiar(one,six)
| familiar(five,six) ),
inference(resolution,[status(thm)],[c54718,c195]) ).
cnf(c54895,plain,
( familiar(five,six)
| ~ familiar(one,X435)
| ~ familiar(X435,six) ),
inference(resolution,[status(thm)],[c54753,three_familiar]) ).
cnf(c55380,plain,
( familiar(five,six)
| ~ familiar(one,two)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c54895,c296]) ).
cnf(c63690,plain,
( familiar(five,six)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c55380,c54968]) ).
cnf(c63756,plain,
( familiar(five,six)
| ~ familiar(two,X473)
| ~ familiar(X473,five) ),
inference(resolution,[status(thm)],[c63690,three_familiar]) ).
cnf(c54870,plain,
( ~ not_familiar(one,three)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c54749,c71]) ).
cnf(c54997,plain,
( familiar(three,five)
| familiar(one,three) ),
inference(resolution,[status(thm)],[c54870,c61]) ).
cnf(c225,plain,
( familiar(three,six)
| ~ not_familiar(three,five)
| familiar(five,six) ),
inference(resolution,[status(thm)],[c187,c100]) ).
cnf(c302,plain,
( familiar(three,six)
| familiar(five,six)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c225,c71]) ).
cnf(c55420,plain,
( familiar(five,six)
| ~ familiar(one,three)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c54895,c302]) ).
cnf(c64538,plain,
( familiar(five,six)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c55420,c54997]) ).
cnf(c64591,plain,
( familiar(five,six)
| ~ familiar(two,three) ),
inference(resolution,[status(thm)],[c64538,c63756]) ).
cnf(c64616,plain,
( familiar(five,six)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c64591,c64]) ).
cnf(c54826,plain,
( ~ not_familiar(one,four)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c54749,c68]) ).
cnf(c54947,plain,
( familiar(four,five)
| familiar(one,four) ),
inference(resolution,[status(thm)],[c54826,c107]) ).
cnf(c205,plain,
( familiar(four,six)
| ~ not_familiar(four,five)
| familiar(five,six) ),
inference(resolution,[status(thm)],[c169,c100]) ).
cnf(c290,plain,
( familiar(four,six)
| familiar(five,six)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c205,c68]) ).
cnf(c55409,plain,
( familiar(five,six)
| ~ familiar(one,four)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c54895,c290]) ).
cnf(c64099,plain,
( familiar(five,six)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c55409,c54947]) ).
cnf(c64156,plain,
( familiar(five,six)
| ~ familiar(two,four) ),
inference(resolution,[status(thm)],[c64099,c63756]) ).
cnf(c64183,plain,
( familiar(five,six)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c64156,c110]) ).
cnf(c64230,plain,
( familiar(five,six)
| ~ not_familiar(two,X477)
| ~ not_familiar(X477,four) ),
inference(resolution,[status(thm)],[c64183,three_not_familiar]) ).
cnf(c64611,plain,
( familiar(five,six)
| ~ familiar(three,X479)
| ~ familiar(X479,five) ),
inference(resolution,[status(thm)],[c64538,three_familiar]) ).
cnf(c64787,plain,
( familiar(five,six)
| ~ familiar(three,four) ),
inference(resolution,[status(thm)],[c64611,c64099]) ).
cnf(c64854,plain,
( familiar(five,six)
| not_familiar(three,four) ),
inference(resolution,[status(thm)],[c64787,c97]) ).
cnf(c64926,plain,
( familiar(five,six)
| ~ not_familiar(two,three) ),
inference(resolution,[status(thm)],[c64854,c64230]) ).
cnf(c64946,plain,
familiar(five,six),
inference(resolution,[status(thm)],[c64926,c64616]) ).
cnf(c64989,plain,
( not_familiar(two,six)
| ~ familiar(two,five) ),
inference(resolution,[status(thm)],[c64946,c172]) ).
cnf(c136,plain,
( familiar(two,five)
| ~ not_familiar(two,X60)
| ~ not_familiar(X60,five) ),
inference(resolution,[status(thm)],[c130,three_not_familiar]) ).
cnf(c182,plain,
( familiar(two,five)
| ~ not_familiar(two,four)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c136,c68]) ).
cnf(c363,plain,
( not_familiar(one,four)
| not_familiar(one,two)
| familiar(two,five)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c232,c182]) ).
cnf(c54940,plain,
( familiar(four,five)
| not_familiar(one,two)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c54826,c363]) ).
cnf(c60647,plain,
( familiar(four,five)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c54940,c54865]) ).
cnf(c181,plain,
( familiar(two,five)
| ~ not_familiar(two,three)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c136,c71]) ).
cnf(c274,plain,
( familiar(two,five)
| familiar(three,five)
| not_familiar(one,three)
| not_familiar(one,two) ),
inference(resolution,[status(thm)],[c181,c152]) ).
cnf(c54978,plain,
( familiar(two,five)
| familiar(three,five)
| not_familiar(one,three) ),
inference(resolution,[status(thm)],[c54865,c274]) ).
cnf(c62198,plain,
( familiar(two,five)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c54978,c54870]) ).
cnf(c62286,plain,
( familiar(two,five)
| ~ familiar(three,X466)
| ~ familiar(X466,five) ),
inference(resolution,[status(thm)],[c62198,three_familiar]) ).
cnf(c62507,plain,
( familiar(two,five)
| ~ familiar(three,four) ),
inference(resolution,[status(thm)],[c62286,c60647]) ).
cnf(c62545,plain,
( familiar(two,five)
| not_familiar(three,four) ),
inference(resolution,[status(thm)],[c62507,c97]) ).
cnf(c64979,plain,
( not_familiar(four,six)
| ~ familiar(four,five) ),
inference(resolution,[status(thm)],[c64946,c167]) ).
cnf(c65098,plain,
( not_familiar(four,six)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c64979,c60647]) ).
cnf(c64985,plain,
( not_familiar(three,six)
| ~ familiar(three,five) ),
inference(resolution,[status(thm)],[c64946,c185]) ).
cnf(c65105,plain,
( not_familiar(three,six)
| familiar(two,five) ),
inference(resolution,[status(thm)],[c64985,c62198]) ).
cnf(c65942,plain,
( familiar(two,five)
| ~ not_familiar(three,X508)
| ~ not_familiar(X508,six) ),
inference(resolution,[status(thm)],[c65105,three_not_familiar]) ).
cnf(c68204,plain,
( familiar(two,five)
| ~ not_familiar(three,four) ),
inference(resolution,[status(thm)],[c65942,c65098]) ).
cnf(c68252,plain,
familiar(two,five),
inference(resolution,[status(thm)],[c68204,c62545]) ).
cnf(c68405,plain,
not_familiar(two,six),
inference(resolution,[status(thm)],[c68252,c64989]) ).
cnf(c68420,plain,
( ~ not_familiar(two,X510)
| ~ not_familiar(X510,six) ),
inference(resolution,[status(thm)],[c68405,three_not_familiar]) ).
cnf(c73,plain,
( familiar(three,five)
| ~ not_familiar(three,X46)
| ~ not_familiar(X46,five) ),
inference(resolution,[status(thm)],[c71,three_not_familiar]) ).
cnf(c96,plain,
( familiar(three,five)
| ~ not_familiar(three,four)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c73,c68]) ).
cnf(c138,plain,
( not_familiar(one,four)
| ~ familiar(one,three)
| not_familiar(three,four) ),
inference(resolution,[status(thm)],[c108,c97]) ).
cnf(c231,plain,
( not_familiar(one,four)
| not_familiar(three,four)
| not_familiar(one,three) ),
inference(resolution,[status(thm)],[c138,c61]) ).
cnf(c346,plain,
( not_familiar(one,four)
| not_familiar(one,three)
| familiar(three,five)
| familiar(four,five) ),
inference(resolution,[status(thm)],[c231,c96]) ).
cnf(c54938,plain,
( familiar(four,five)
| not_familiar(one,three)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c54826,c346]) ).
cnf(c60111,plain,
( familiar(four,five)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c54938,c54870]) ).
cnf(c60824,plain,
( familiar(four,five)
| ~ familiar(two,X462)
| ~ familiar(X462,five) ),
inference(resolution,[status(thm)],[c60647,three_familiar]) ).
cnf(c60950,plain,
( familiar(four,five)
| ~ familiar(two,three) ),
inference(resolution,[status(thm)],[c60824,c60111]) ).
cnf(c60991,plain,
( familiar(four,five)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c60950,c64]) ).
cnf(c65091,plain,
( not_familiar(four,six)
| not_familiar(two,three) ),
inference(resolution,[status(thm)],[c64979,c60991]) ).
cnf(c65086,plain,
( not_familiar(four,six)
| familiar(three,five) ),
inference(resolution,[status(thm)],[c64979,c60111]) ).
cnf(c65552,plain,
( not_familiar(four,six)
| not_familiar(three,six) ),
inference(resolution,[status(thm)],[c65086,c64985]) ).
cnf(c68469,plain,
( ~ not_familiar(two,three)
| not_familiar(four,six) ),
inference(resolution,[status(thm)],[c68420,c65552]) ).
cnf(c68664,plain,
not_familiar(four,six),
inference(resolution,[status(thm)],[c68469,c65091]) ).
cnf(c68676,plain,
~ not_familiar(two,four),
inference(resolution,[status(thm)],[c68664,c68420]) ).
cnf(c68683,plain,
not_familiar(two,three),
inference(resolution,[status(thm)],[c68676,c58871]) ).
cnf(c62243,plain,
( familiar(three,five)
| ~ familiar(two,X465)
| ~ familiar(X465,five) ),
inference(resolution,[status(thm)],[c62198,three_familiar]) ).
cnf(c62290,plain,
( familiar(three,five)
| ~ familiar(two,four) ),
inference(resolution,[status(thm)],[c62243,c60111]) ).
cnf(c62361,plain,
( familiar(three,five)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c62290,c110]) ).
cnf(c65108,plain,
( not_familiar(three,six)
| not_familiar(two,four) ),
inference(resolution,[status(thm)],[c64985,c62361]) ).
cnf(c68690,plain,
not_familiar(three,six),
inference(resolution,[status(thm)],[c68676,c65108]) ).
cnf(c68771,plain,
~ not_familiar(two,three),
inference(resolution,[status(thm)],[c68690,c68420]) ).
cnf(c68809,plain,
$false,
inference(resolution,[status(thm)],[c68771,c68683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : PUZ028-5 : TPTP v8.1.2. Released v2.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n012.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 20:37:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 61.72/61.91 % Version: 1.5
% 61.72/61.91 % SZS status Unsatisfiable
% 61.72/61.91 % SZS output start CNFRefutation
% See solution above
% 61.72/61.91
% 61.72/61.91 % Initial clauses : 15
% 61.72/61.91 % Processed clauses : 1681
% 61.72/61.91 % Factors computed : 7
% 61.72/61.91 % Resolvents computed: 68803
% 61.72/61.91 % Tautologies deleted: 153
% 61.72/61.91 % Forward subsumed : 1583
% 61.72/61.91 % Backward subsumed : 1365
% 61.72/61.91 % -------- CPU Time ---------
% 61.72/61.91 % User time : 61.349 s
% 61.72/61.91 % System time : 0.211 s
% 61.72/61.91 % Total time : 61.560 s
%------------------------------------------------------------------------------