%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ028-6 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:31:54 PM UTC 2026
% Result : Unsatisfiable 58.97s 27.49s
% Output : Proof 58.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 84
% Number of leaves : 41
% Syntax : Number of formulae : 544 ( 119 unt; 0 def)
% Number of atoms : 1501 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 1265 ( 308 ~; 957 |; 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 : 105 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f36,axiom,
( ~ not_equal(X,Y)
| ~ person(Y)
| ~ person(X)
| not_familiar(X,Y)
| familiar(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',familiar_or_not) ).
fof(f36_nnf,plain,
! [X,Y] :
( ~ not_equal(X,Y)
| ~ person(Y)
| ~ person(X)
| not_familiar(X,Y)
| familiar(X,Y) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X,Y] :
( ~ not_equal(X,Y)
| ~ person(Y)
| ~ person(X)
| not_familiar(X,Y)
| familiar(X,Y) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( ~ not_equal(X0,X1)
| ~ person(X1)
| ~ person(X0)
| not_familiar(X0,X1)
| familiar(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(f2,axiom,
person(n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person_3) ).
fof(f2_nnf,plain,
person(n3),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
person(n3),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(p48,plain,
( ~ not_equal(n3,X0)
| ~ person(X0)
| not_familiar(n3,X0)
| familiar(n3,X0) ),
inference(resolution,[status(thm)],[c36,c2]) ).
cnf(f3,axiom,
person(n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person_4) ).
fof(f3_nnf,plain,
person(n4),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
person(n4),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(p74,plain,
( ~ not_equal(n3,n4)
| not_familiar(n3,n4)
| familiar(n3,n4) ),
inference(resolution,[status(thm)],[p48,c3]) ).
cnf(f18,axiom,
not_equal(n3,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_3_4) ).
fof(f18_nnf,plain,
not_equal(n3,n4),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
not_equal(n3,n4),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(p149,plain,
( not_familiar(n3,n4)
| familiar(n3,n4) ),
inference(resolution,[status(thm)],[p74,c18]) ).
cnf(f0,axiom,
person(n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person_1) ).
fof(f0_nnf,plain,
person(n1),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
person(n1),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(p46,plain,
( ~ not_equal(n1,X0)
| ~ person(X0)
| not_familiar(n1,X0)
| familiar(n1,X0) ),
inference(resolution,[status(thm)],[c36,c0]) ).
cnf(p60,plain,
( ~ not_equal(n1,n4)
| not_familiar(n1,n4)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p46,c3]) ).
cnf(f8,axiom,
not_equal(n1,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_1_4) ).
fof(f8_nnf,plain,
not_equal(n1,n4),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
not_equal(n1,n4),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(p88,plain,
( not_familiar(n1,n4)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p60,c8]) ).
cnf(f38,axiom,
( not_familiar(X2,X1)
| ~ not_familiar(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_not_familiar) ).
fof(f38_nnf,plain,
! [X1,X2] :
( not_familiar(X2,X1)
| ~ not_familiar(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X1,X2] :
( not_familiar(X2,X1)
| ~ not_familiar(X1,X2) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( not_familiar(X1,X0)
| ~ not_familiar(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p95,plain,
( not_familiar(n4,n1)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p88,c38]) ).
cnf(f40,negated_conjecture,
( ~ not_familiar(X3,X1)
| ~ not_familiar(X2,X3)
| ~ not_familiar(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',three_not_familiar) ).
fof(f40_nnf,plain,
! [X1,X2,X3] :
( ~ not_familiar(X3,X1)
| ~ not_familiar(X2,X3)
| ~ not_familiar(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X1,X2,X3] :
( ~ not_familiar(X3,X1)
| ~ not_familiar(X2,X3)
| ~ not_familiar(X1,X2) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( ~ not_familiar(X2,X0)
| ~ not_familiar(X1,X2)
| ~ not_familiar(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p103,plain,
( ~ not_familiar(X0,n4)
| ~ not_familiar(n1,X0)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p95,c40]) ).
cnf(p59,plain,
( ~ not_equal(n1,n3)
| not_familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p46,c2]) ).
cnf(f7,axiom,
not_equal(n1,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_1_3) ).
fof(f7_nnf,plain,
not_equal(n1,n3),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
not_equal(n1,n3),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(p77,plain,
( not_familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p59,c7]) ).
cnf(p105,plain,
( familiar(n1,n3)
| ~ not_familiar(n3,n4)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p103,p77]) ).
cnf(p283,plain,
( familiar(n1,n3)
| familiar(n1,n4)
| familiar(n3,n4) ),
inference(resolution,[status(thm)],[p149,p105]) ).
cnf(f39,negated_conjecture,
( ~ familiar(X3,X1)
| ~ familiar(X2,X3)
| ~ familiar(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',three_familiar) ).
fof(f39_nnf,plain,
! [X1,X2,X3] :
( ~ familiar(X3,X1)
| ~ familiar(X2,X3)
| ~ familiar(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X1,X2,X3] :
( ~ familiar(X3,X1)
| ~ familiar(X2,X3)
| ~ familiar(X1,X2) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( ~ familiar(X2,X0)
| ~ familiar(X1,X2)
| ~ familiar(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p299,plain,
( ~ familiar(X0,n3)
| ~ familiar(n4,X0)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p283,c39]) ).
cnf(p49,plain,
( ~ not_equal(n4,X0)
| ~ person(X0)
| not_familiar(n4,X0)
| familiar(n4,X0) ),
inference(resolution,[status(thm)],[c36,c3]) ).
cnf(f5,axiom,
person(n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person_6) ).
fof(f5_nnf,plain,
person(n6),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
person(n6),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p85,plain,
( ~ not_equal(n4,n6)
| not_familiar(n4,n6)
| familiar(n4,n6) ),
inference(resolution,[status(thm)],[p49,c5]) ).
cnf(f25,axiom,
not_equal(n4,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_4_6) ).
fof(f25_nnf,plain,
not_equal(n4,n6),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
not_equal(n4,n6),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(p185,plain,
( not_familiar(n4,n6)
| familiar(n4,n6) ),
inference(resolution,[status(thm)],[p85,c25]) ).
cnf(p62,plain,
( ~ not_equal(n1,n6)
| not_familiar(n1,n6)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p46,c5]) ).
cnf(f10,axiom,
not_equal(n1,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_1_6) ).
fof(f10_nnf,plain,
not_equal(n1,n6),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
not_equal(n1,n6),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(p112,plain,
( not_familiar(n1,n6)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p62,c10]) ).
cnf(p119,plain,
( not_familiar(n6,n1)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p112,c38]) ).
cnf(p133,plain,
( ~ not_familiar(X0,n6)
| ~ not_familiar(n1,X0)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p119,c40]) ).
cnf(p136,plain,
( familiar(n1,n4)
| ~ not_familiar(n4,n6)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p133,p88]) ).
cnf(p355,plain,
( familiar(n1,n4)
| familiar(n1,n6)
| familiar(n4,n6) ),
inference(resolution,[status(thm)],[p185,p136]) ).
cnf(p666,plain,
( familiar(n1,n4)
| familiar(n1,n6)
| ~ familiar(n6,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p299,p355]) ).
cnf(p1731,plain,
( familiar(n1,n6)
| ~ familiar(n6,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p666]) ).
cnf(p76,plain,
( ~ not_equal(n3,n6)
| not_familiar(n3,n6)
| familiar(n3,n6) ),
inference(resolution,[status(thm)],[p48,c5]) ).
cnf(f20,axiom,
not_equal(n3,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_3_6) ).
fof(f20_nnf,plain,
not_equal(n3,n6),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
not_equal(n3,n6),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(p161,plain,
( not_familiar(n3,n6)
| familiar(n3,n6) ),
inference(resolution,[status(thm)],[p76,c20]) ).
cnf(p135,plain,
( familiar(n1,n3)
| ~ not_familiar(n3,n6)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p133,p77]) ).
cnf(p297,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n3,n6) ),
inference(resolution,[status(thm)],[p161,p135]) ).
cnf(f37,axiom,
( familiar(X2,X1)
| ~ familiar(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_familiar) ).
fof(f37_nnf,plain,
! [X1,X2] :
( familiar(X2,X1)
| ~ familiar(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X1,X2] :
( familiar(X2,X1)
| ~ familiar(X1,X2) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( familiar(X1,X0)
| ~ familiar(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p339,plain,
( familiar(n6,n3)
| familiar(n1,n3)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p297,c37]) ).
cnf(p3588,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p1731,p339]) ).
cnf(p7388,plain,
( familiar(n1,n6)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p3588]) ).
cnf(p7404,plain,
( familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p7388]) ).
cnf(f4,axiom,
person(n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person_5) ).
fof(f4_nnf,plain,
person(n5),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
person(n5),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(p84,plain,
( ~ not_equal(n4,n5)
| not_familiar(n4,n5)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p49,c4]) ).
cnf(f24,axiom,
not_equal(n4,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_4_5) ).
fof(f24_nnf,plain,
not_equal(n4,n5),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
not_equal(n4,n5),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(p182,plain,
( not_familiar(n4,n5)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p84,c24]) ).
cnf(p61,plain,
( ~ not_equal(n1,n5)
| not_familiar(n1,n5)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p46,c4]) ).
cnf(f9,axiom,
not_equal(n1,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_1_5) ).
fof(f9_nnf,plain,
not_equal(n1,n5),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
not_equal(n1,n5),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(p106,plain,
( not_familiar(n1,n5)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p61,c9]) ).
cnf(p108,plain,
( not_familiar(n5,n1)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p106,c38]) ).
cnf(p113,plain,
( ~ not_familiar(X0,n5)
| ~ not_familiar(n1,X0)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p108,c40]) ).
cnf(p116,plain,
( familiar(n1,n4)
| ~ not_familiar(n4,n5)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p113,p88]) ).
cnf(p348,plain,
( familiar(n1,n4)
| familiar(n1,n5)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p182,p116]) ).
cnf(p665,plain,
( familiar(n1,n4)
| familiar(n1,n5)
| ~ familiar(n5,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p299,p348]) ).
cnf(p1730,plain,
( familiar(n1,n5)
| ~ familiar(n5,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p665]) ).
cnf(p75,plain,
( ~ not_equal(n3,n5)
| not_familiar(n3,n5)
| familiar(n3,n5) ),
inference(resolution,[status(thm)],[p48,c4]) ).
cnf(f19,axiom,
not_equal(n3,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_3_5) ).
fof(f19_nnf,plain,
not_equal(n3,n5),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
not_equal(n3,n5),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(p158,plain,
( not_familiar(n3,n5)
| familiar(n3,n5) ),
inference(resolution,[status(thm)],[p75,c19]) ).
cnf(p115,plain,
( familiar(n1,n3)
| ~ not_familiar(n3,n5)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p113,p77]) ).
cnf(p290,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| familiar(n3,n5) ),
inference(resolution,[status(thm)],[p158,p115]) ).
cnf(p320,plain,
( familiar(n5,n3)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p290,c37]) ).
cnf(p3580,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p1730,p320]) ).
cnf(p7339,plain,
( familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p3580]) ).
cnf(p7341,plain,
( familiar(n1,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p7339]) ).
cnf(p7343,plain,
( familiar(n5,n1)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p7341,c37]) ).
cnf(p7379,plain,
( ~ familiar(X0,n5)
| ~ familiar(n1,X0)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p7343,c39]) ).
cnf(p7454,plain,
( ~ familiar(n6,n5)
| familiar(n1,n3)
| familiar(n1,n4)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p7404,p7379]) ).
cnf(p11018,plain,
( ~ familiar(n6,n5)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p7454]) ).
cnf(p11020,plain,
( ~ familiar(n6,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p11018]) ).
cnf(f1,axiom,
person(n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',person_2) ).
fof(f1_nnf,plain,
person(n2),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
person(n2),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(p47,plain,
( ~ not_equal(n2,X0)
| ~ person(X0)
| not_familiar(n2,X0)
| familiar(n2,X0) ),
inference(resolution,[status(thm)],[c36,c1]) ).
cnf(p64,plain,
( ~ not_equal(n2,n1)
| not_familiar(n2,n1)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p47,c0]) ).
cnf(f11,axiom,
not_equal(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_2_1) ).
fof(f11_nnf,plain,
not_equal(n2,n1),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
not_equal(n2,n1),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p117,plain,
( not_familiar(n2,n1)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p64,c11]) ).
cnf(p127,plain,
( not_familiar(n1,n2)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p117,c38]) ).
cnf(p66,plain,
( ~ not_equal(n2,n4)
| not_familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p47,c3]) ).
cnf(f13,axiom,
not_equal(n2,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_2_4) ).
fof(f13_nnf,plain,
not_equal(n2,n4),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
not_equal(n2,n4),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(p125,plain,
( not_familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p66,c13]) ).
cnf(p150,plain,
( ~ not_familiar(X0,n2)
| ~ not_familiar(n4,X0)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p125,c40]) ).
cnf(p154,plain,
( familiar(n1,n4)
| ~ not_familiar(n1,n2)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p150,p95]) ).
cnf(p171,plain,
( familiar(n1,n4)
| familiar(n2,n4)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p127,p154]) ).
cnf(p178,plain,
( familiar(n4,n2)
| familiar(n1,n4)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p171,c37]) ).
cnf(p181,plain,
( ~ familiar(X0,n4)
| ~ familiar(n2,X0)
| familiar(n1,n4)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p178,c39]) ).
cnf(p65,plain,
( ~ not_equal(n2,n3)
| not_familiar(n2,n3)
| familiar(n2,n3) ),
inference(resolution,[status(thm)],[p47,c2]) ).
cnf(f12,axiom,
not_equal(n2,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_2_3) ).
fof(f12_nnf,plain,
not_equal(n2,n3),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
not_equal(n2,n3),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(p124,plain,
( not_familiar(n2,n3)
| familiar(n2,n3) ),
inference(resolution,[status(thm)],[p65,c12]) ).
cnf(p140,plain,
( ~ not_familiar(X0,n2)
| ~ not_familiar(n3,X0)
| familiar(n2,n3) ),
inference(resolution,[status(thm)],[p124,c40]) ).
cnf(p79,plain,
( not_familiar(n3,n1)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p77,c38]) ).
cnf(p144,plain,
( familiar(n1,n3)
| ~ not_familiar(n1,n2)
| familiar(n2,n3) ),
inference(resolution,[status(thm)],[p140,p79]) ).
cnf(p170,plain,
( familiar(n1,n3)
| familiar(n2,n3)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p127,p144]) ).
cnf(p184,plain,
( familiar(n1,n3)
| familiar(n2,n1)
| ~ familiar(n3,n4)
| familiar(n1,n4)
| familiar(n2,n1) ),
inference(resolution,[status(thm)],[p181,p170]) ).
cnf(p187,plain,
( familiar(n1,n3)
| ~ familiar(n3,n4)
| familiar(n1,n4)
| familiar(n2,n1) ),
inference(factoring,[status(thm)],[p184]) ).
cnf(p304,plain,
( familiar(n1,n3)
| familiar(n1,n4)
| familiar(n2,n1)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p283,p187]) ).
cnf(p687,plain,
( familiar(n1,n3)
| familiar(n2,n1)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p304]) ).
cnf(p1841,plain,
( familiar(n2,n1)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p687]) ).
cnf(p1851,plain,
( ~ familiar(X0,n2)
| ~ familiar(n1,X0)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p1841,c39]) ).
cnf(p7411,plain,
( ~ familiar(n6,n2)
| familiar(n1,n3)
| familiar(n1,n4)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p7404,p1851]) ).
cnf(p10886,plain,
( ~ familiar(n6,n2)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p7411]) ).
cnf(p10888,plain,
( ~ familiar(n6,n2)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p10886]) ).
cnf(p50,plain,
( ~ not_equal(n5,X0)
| ~ person(X0)
| not_familiar(n5,X0)
| familiar(n5,X0) ),
inference(resolution,[status(thm)],[c36,c4]) ).
cnf(p93,plain,
( ~ not_equal(n5,n6)
| not_familiar(n5,n6)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p50,c5]) ).
cnf(f30,axiom,
not_equal(n5,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_5_6) ).
fof(f30_nnf,plain,
not_equal(n5,n6),
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
not_equal(n5,n6),
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(p219,plain,
( not_familiar(n5,n6)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p93,c30]) ).
cnf(p67,plain,
( ~ not_equal(n2,n5)
| not_familiar(n2,n5)
| familiar(n2,n5) ),
inference(resolution,[status(thm)],[p47,c4]) ).
cnf(f14,axiom,
not_equal(n2,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_2_5) ).
fof(f14_nnf,plain,
not_equal(n2,n5),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
not_equal(n2,n5),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(p132,plain,
( not_familiar(n2,n5)
| familiar(n2,n5) ),
inference(resolution,[status(thm)],[p67,c14]) ).
cnf(p189,plain,
( ~ not_familiar(X0,n2)
| ~ not_familiar(n5,X0)
| familiar(n2,n5) ),
inference(resolution,[status(thm)],[p132,c40]) ).
cnf(p433,plain,
( ~ not_familiar(n6,n2)
| familiar(n2,n5)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p219,p189]) ).
cnf(p51,plain,
( ~ not_equal(n6,X0)
| ~ person(X0)
| not_familiar(n6,X0)
| familiar(n6,X0) ),
inference(resolution,[status(thm)],[c36,c5]) ).
cnf(p99,plain,
( ~ not_equal(n6,n2)
| not_familiar(n6,n2)
| familiar(n6,n2) ),
inference(resolution,[status(thm)],[p51,c1]) ).
cnf(f32,axiom,
not_equal(n6,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_6_2) ).
fof(f32_nnf,plain,
not_equal(n6,n2),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
not_equal(n6,n2),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(p225,plain,
( not_familiar(n6,n2)
| familiar(n6,n2) ),
inference(resolution,[status(thm)],[p99,c32]) ).
cnf(p587,plain,
( familiar(n6,n2)
| familiar(n2,n5)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p433,p225]) ).
cnf(p10891,plain,
( familiar(n2,n5)
| familiar(n5,n6)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p10888,p587]) ).
cnf(p10927,plain,
( familiar(n6,n5)
| familiar(n2,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p10891,c37]) ).
cnf(p11027,plain,
( familiar(n2,n5)
| familiar(n1,n3)
| familiar(n1,n4)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p11020,p10927]) ).
cnf(p15267,plain,
( familiar(n2,n5)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p11027]) ).
cnf(p15271,plain,
( familiar(n2,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p15267]) ).
cnf(p83,plain,
( ~ not_equal(n4,n3)
| not_familiar(n4,n3)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p49,c2]) ).
cnf(f23,axiom,
not_equal(n4,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_4_3) ).
fof(f23_nnf,plain,
not_equal(n4,n3),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
not_equal(n4,n3),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(p179,plain,
( not_familiar(n4,n3)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p83,c23]) ).
cnf(p72,plain,
( ~ not_equal(n3,n1)
| not_familiar(n3,n1)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p48,c0]) ).
cnf(f16,axiom,
not_equal(n3,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_3_1) ).
fof(f16_nnf,plain,
not_equal(n3,n1),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
not_equal(n3,n1),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(p139,plain,
( not_familiar(n3,n1)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p72,c16]) ).
cnf(p253,plain,
( ~ not_familiar(X0,n3)
| ~ not_familiar(n1,X0)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p139,c40]) ).
cnf(p259,plain,
( familiar(n1,n4)
| ~ not_familiar(n4,n3)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p253,p88]) ).
cnf(p335,plain,
( familiar(n1,n4)
| familiar(n3,n1)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p179,p259]) ).
cnf(p58,plain,
( ~ not_equal(n1,n2)
| not_familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p46,c1]) ).
cnf(f6,axiom,
not_equal(n1,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_1_2) ).
fof(f6_nnf,plain,
not_equal(n1,n2),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
not_equal(n1,n2),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(p63,plain,
( not_familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p58,c6]) ).
cnf(p104,plain,
( familiar(n1,n2)
| ~ not_familiar(n2,n4)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p103,p63]) ).
cnf(p153,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p125,p104]) ).
cnf(p155,plain,
( ~ familiar(X0,n2)
| ~ familiar(n4,X0)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p153,c39]) ).
cnf(p406,plain,
( ~ familiar(n3,n2)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p335,p155]) ).
cnf(p949,plain,
( ~ familiar(n3,n2)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(factoring,[status(thm)],[p406]) ).
cnf(p254,plain,
( not_familiar(n1,n3)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p139,c38]) ).
cnf(p73,plain,
( ~ not_equal(n3,n2)
| not_familiar(n3,n2)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p48,c1]) ).
cnf(f17,axiom,
not_equal(n3,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_3_2) ).
fof(f17_nnf,plain,
not_equal(n3,n2),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
not_equal(n3,n2),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(p147,plain,
( not_familiar(n3,n2)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p73,c17]) ).
cnf(p267,plain,
( ~ not_familiar(X0,n3)
| ~ not_familiar(n2,X0)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p147,c40]) ).
cnf(p70,plain,
( not_familiar(n2,n1)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p63,c38]) ).
cnf(p275,plain,
( familiar(n1,n2)
| ~ not_familiar(n1,n3)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p267,p70]) ).
cnf(p577,plain,
( familiar(n1,n2)
| familiar(n3,n2)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p254,p275]) ).
cnf(p2267,plain,
( familiar(n1,n2)
| familiar(n3,n1)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(resolution,[status(thm)],[p949,p577]) ).
cnf(p5924,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(factoring,[status(thm)],[p2267]) ).
cnf(p5926,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n3,n1) ),
inference(factoring,[status(thm)],[p5924]) ).
cnf(p5927,plain,
( ~ familiar(X0,n3)
| ~ familiar(n1,X0)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p5926,c39]) ).
cnf(p114,plain,
( familiar(n1,n2)
| ~ not_familiar(n2,n5)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p113,p63]) ).
cnf(p192,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n2,n5) ),
inference(resolution,[status(thm)],[p132,p114]) ).
cnf(p197,plain,
( familiar(n5,n2)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p192,c37]) ).
cnf(p207,plain,
( ~ familiar(X0,n5)
| ~ familiar(n2,X0)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p197,c39]) ).
cnf(p211,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| ~ familiar(n4,n5)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p207,p153]) ).
cnf(p224,plain,
( familiar(n1,n4)
| ~ familiar(n4,n5)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p211]) ).
cnf(p439,plain,
( familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p348,p224]) ).
cnf(p1066,plain,
( familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p439]) ).
cnf(p2615,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p1066]) ).
cnf(p5941,plain,
( familiar(n1,n2)
| familiar(n1,n4)
| ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p5927,p2615]) ).
cnf(p9441,plain,
( familiar(n1,n2)
| ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p5941]) ).
cnf(p9443,plain,
( ~ familiar(n5,n3)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p9441]) ).
cnf(p68,plain,
( ~ not_equal(n2,n6)
| not_familiar(n2,n6)
| familiar(n2,n6) ),
inference(resolution,[status(thm)],[p47,c5]) ).
cnf(f15,axiom,
not_equal(n2,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_2_6) ).
fof(f15_nnf,plain,
not_equal(n2,n6),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
not_equal(n2,n6),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(p138,plain,
( not_familiar(n2,n6)
| familiar(n2,n6) ),
inference(resolution,[status(thm)],[p68,c15]) ).
cnf(p134,plain,
( familiar(n1,n2)
| ~ not_familiar(n2,n6)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p133,p63]) ).
cnf(p232,plain,
( familiar(n1,n2)
| familiar(n1,n6)
| familiar(n2,n6) ),
inference(resolution,[status(thm)],[p138,p134]) ).
cnf(p156,plain,
( familiar(n4,n2)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p153,c37]) ).
cnf(p159,plain,
( ~ familiar(X0,n4)
| ~ familiar(n2,X0)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p156,c39]) ).
cnf(p240,plain,
( ~ familiar(n6,n4)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p232,p159]) ).
cnf(p505,plain,
( ~ familiar(n6,n4)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p240]) ).
cnf(p455,plain,
( familiar(n6,n4)
| familiar(n1,n4)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p355,c37]) ).
cnf(p1228,plain,
( familiar(n1,n4)
| familiar(n1,n6)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p505,p455]) ).
cnf(p4371,plain,
( familiar(n1,n4)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p1228]) ).
cnf(p4375,plain,
( familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p4371]) ).
cnf(p2617,plain,
( familiar(n5,n1)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p2615,c37]) ).
cnf(p2626,plain,
( ~ familiar(X0,n5)
| ~ familiar(n1,X0)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p2617,c39]) ).
cnf(p4385,plain,
( ~ familiar(n6,n5)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4375,p2626]) ).
cnf(p8598,plain,
( ~ familiar(n6,n5)
| familiar(n1,n4)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p4385]) ).
cnf(p8600,plain,
( ~ familiar(n6,n5)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p8598]) ).
cnf(p91,plain,
( ~ not_equal(n5,n3)
| not_familiar(n5,n3)
| familiar(n5,n3) ),
inference(resolution,[status(thm)],[p50,c2]) ).
cnf(f28,axiom,
not_equal(n5,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_5_3) ).
fof(f28_nnf,plain,
not_equal(n5,n3),
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
not_equal(n5,n3),
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(p208,plain,
( not_familiar(n5,n3)
| familiar(n5,n3) ),
inference(resolution,[status(thm)],[p91,c28]) ).
cnf(p397,plain,
( ~ not_familiar(X0,n5)
| ~ not_familiar(n3,X0)
| familiar(n5,n3) ),
inference(resolution,[status(thm)],[p208,c40]) ).
cnf(p521,plain,
( familiar(n3,n6)
| ~ not_familiar(n6,n5)
| familiar(n5,n3) ),
inference(resolution,[status(thm)],[p397,p161]) ).
cnf(p102,plain,
( ~ not_equal(n6,n5)
| not_familiar(n6,n5)
| familiar(n6,n5) ),
inference(resolution,[status(thm)],[p51,c4]) ).
cnf(f35,axiom,
not_equal(n6,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_6_5) ).
fof(f35_nnf,plain,
not_equal(n6,n5),
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
not_equal(n6,n5),
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(p250,plain,
( not_familiar(n6,n5)
| familiar(n6,n5) ),
inference(resolution,[status(thm)],[p102,c35]) ).
cnf(p747,plain,
( familiar(n6,n5)
| familiar(n3,n6)
| familiar(n5,n3) ),
inference(resolution,[status(thm)],[p521,p250]) ).
cnf(p8603,plain,
( familiar(n3,n6)
| familiar(n5,n3)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p8600,p747]) ).
cnf(p9448,plain,
( familiar(n3,n6)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p9443,p8603]) ).
cnf(p13579,plain,
( familiar(n3,n6)
| familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p9448]) ).
cnf(p13581,plain,
( familiar(n3,n6)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p13579]) ).
cnf(p86,plain,
( ~ not_familiar(X0,n3)
| ~ not_familiar(n1,X0)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p79,c40]) ).
cnf(p87,plain,
( familiar(n1,n2)
| ~ not_familiar(n2,n3)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p86,p63]) ).
cnf(p143,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| familiar(n2,n3) ),
inference(resolution,[status(thm)],[p124,p87]) ).
cnf(p146,plain,
( familiar(n3,n2)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p143,c37]) ).
cnf(p148,plain,
( ~ familiar(X0,n3)
| ~ familiar(n2,X0)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p146,c39]) ).
cnf(p239,plain,
( ~ familiar(n6,n3)
| familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p232,p148]) ).
cnf(p502,plain,
( ~ familiar(n6,n3)
| familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p239]) ).
cnf(p1223,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p502,p339]) ).
cnf(p4313,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p1223]) ).
cnf(p4325,plain,
( familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p4313]) ).
cnf(p210,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| ~ familiar(n3,n5)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p207,p143]) ).
cnf(p223,plain,
( familiar(n1,n3)
| ~ familiar(n3,n5)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p210]) ).
cnf(p323,plain,
( familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p290,p223]) ).
cnf(p743,plain,
( familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p323]) ).
cnf(p1978,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p743]) ).
cnf(p1980,plain,
( familiar(n5,n1)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p1978,c37]) ).
cnf(p1987,plain,
( ~ familiar(X0,n5)
| ~ familiar(n1,X0)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p1980,c39]) ).
cnf(p4337,plain,
( ~ familiar(n6,n5)
| familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4325,p1987]) ).
cnf(p8481,plain,
( ~ familiar(n6,n5)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p4337]) ).
cnf(p8483,plain,
( ~ familiar(n6,n5)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p8481]) ).
cnf(p160,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| ~ familiar(n3,n4)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p159,p143]) ).
cnf(p163,plain,
( familiar(n1,n3)
| ~ familiar(n3,n4)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p160]) ).
cnf(p302,plain,
( familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n4)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p283,p163]) ).
cnf(p675,plain,
( familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p302]) ).
cnf(p1773,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p675]) ).
cnf(p1844,plain,
( familiar(n4,n1)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p1773,c37]) ).
cnf(p1856,plain,
( ~ familiar(X0,n4)
| ~ familiar(n1,X0)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p1844,c39]) ).
cnf(p4336,plain,
( ~ familiar(n6,n4)
| familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4325,p1856]) ).
cnf(p8372,plain,
( ~ familiar(n6,n4)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p4336]) ).
cnf(p8374,plain,
( ~ familiar(n6,n4)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p8372]) ).
cnf(p345,plain,
( ~ not_familiar(X0,n4)
| ~ not_familiar(n5,X0)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p182,c40]) ).
cnf(p435,plain,
( ~ not_familiar(n6,n4)
| familiar(n4,n5)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p219,p345]) ).
cnf(p101,plain,
( ~ not_equal(n6,n4)
| not_familiar(n6,n4)
| familiar(n6,n4) ),
inference(resolution,[status(thm)],[p51,c3]) ).
cnf(f34,axiom,
not_equal(n6,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_6_4) ).
fof(f34_nnf,plain,
not_equal(n6,n4),
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c34,plain,
not_equal(n6,n4),
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(p236,plain,
( not_familiar(n6,n4)
| familiar(n6,n4) ),
inference(resolution,[status(thm)],[p101,c34]) ).
cnf(p590,plain,
( familiar(n6,n4)
| familiar(n4,n5)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p435,p236]) ).
cnf(p8381,plain,
( familiar(n4,n5)
| familiar(n5,n6)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p8374,p590]) ).
cnf(p8427,plain,
( familiar(n6,n5)
| familiar(n4,n5)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p8381,c37]) ).
cnf(p8496,plain,
( familiar(n4,n5)
| familiar(n1,n3)
| familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p8483,p8427]) ).
cnf(p12597,plain,
( familiar(n4,n5)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p8496]) ).
cnf(p12599,plain,
( familiar(n4,n5)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p12597]) ).
cnf(p3649,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| ~ familiar(n4,n5)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p1987,p1773]) ).
cnf(p7622,plain,
( familiar(n1,n2)
| ~ familiar(n4,n5)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p3649]) ).
cnf(p7624,plain,
( ~ familiar(n4,n5)
| familiar(n1,n2)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p7622]) ).
cnf(p12606,plain,
( familiar(n1,n2)
| familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p12599,p7624]) ).
cnf(p12612,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p12606]) ).
cnf(p12616,plain,
( familiar(n1,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p12612]) ).
cnf(p4377,plain,
( familiar(n6,n1)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4375,c37]) ).
cnf(p4386,plain,
( ~ familiar(X0,n6)
| ~ familiar(n1,X0)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4377,c39]) ).
cnf(p12637,plain,
( ~ familiar(n3,n6)
| familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p12616,p4386]) ).
cnf(p12858,plain,
( ~ familiar(n3,n6)
| familiar(n1,n4)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p12637]) ).
cnf(p13587,plain,
( familiar(n1,n4)
| familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p13581,p12858]) ).
cnf(p13619,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p13587]) ).
cnf(p13621,plain,
( familiar(n1,n2)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p13619]) ).
cnf(p12618,plain,
( familiar(n3,n1)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p12616,c37]) ).
cnf(p12658,plain,
( ~ familiar(X0,n3)
| ~ familiar(n1,X0)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p12618,c39]) ).
cnf(p13666,plain,
( ~ familiar(n4,n3)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p13621,p12658]) ).
cnf(p13709,plain,
( ~ familiar(n4,n3)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p13666]) ).
cnf(p81,plain,
( ~ not_equal(n4,n1)
| not_familiar(n4,n1)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p49,c0]) ).
cnf(f21,axiom,
not_equal(n4,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_4_1) ).
fof(f21_nnf,plain,
not_equal(n4,n1),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
not_equal(n4,n1),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(p164,plain,
( not_familiar(n4,n1)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p81,c21]) ).
cnf(p311,plain,
( ~ not_familiar(X0,n4)
| ~ not_familiar(n1,X0)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p164,c40]) ).
cnf(p360,plain,
( familiar(n1,n5)
| ~ not_familiar(n5,n4)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p311,p106]) ).
cnf(p92,plain,
( ~ not_equal(n5,n4)
| not_familiar(n5,n4)
| familiar(n5,n4) ),
inference(resolution,[status(thm)],[p50,c3]) ).
cnf(f29,axiom,
not_equal(n5,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_5_4) ).
fof(f29_nnf,plain,
not_equal(n5,n4),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
not_equal(n5,n4),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(p214,plain,
( not_familiar(n5,n4)
| familiar(n5,n4) ),
inference(resolution,[status(thm)],[p92,c29]) ).
cnf(p465,plain,
( familiar(n5,n4)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p360,p214]) ).
cnf(p196,plain,
( ~ familiar(X0,n2)
| ~ familiar(n5,X0)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p192,c39]) ).
cnf(p642,plain,
( ~ familiar(n4,n2)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p465,p196]) ).
cnf(p1710,plain,
( ~ familiar(n4,n2)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(factoring,[status(thm)],[p642]) ).
cnf(p312,plain,
( not_familiar(n1,n4)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p164,c38]) ).
cnf(p82,plain,
( ~ not_equal(n4,n2)
| not_familiar(n4,n2)
| familiar(n4,n2) ),
inference(resolution,[status(thm)],[p49,c1]) ).
cnf(f22,axiom,
not_equal(n4,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_4_2) ).
fof(f22_nnf,plain,
not_equal(n4,n2),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
not_equal(n4,n2),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(p174,plain,
( not_familiar(n4,n2)
| familiar(n4,n2) ),
inference(resolution,[status(thm)],[p82,c22]) ).
cnf(p325,plain,
( ~ not_familiar(X0,n4)
| ~ not_familiar(n2,X0)
| familiar(n4,n2) ),
inference(resolution,[status(thm)],[p174,c40]) ).
cnf(p380,plain,
( familiar(n1,n2)
| ~ not_familiar(n1,n4)
| familiar(n4,n2) ),
inference(resolution,[status(thm)],[p325,p70]) ).
cnf(p698,plain,
( familiar(n1,n2)
| familiar(n4,n2)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p312,p380]) ).
cnf(p3571,plain,
( familiar(n1,n2)
| familiar(n4,n1)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p1710,p698]) ).
cnf(p7279,plain,
( familiar(n1,n2)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(factoring,[status(thm)],[p3571]) ).
cnf(p7281,plain,
( familiar(n1,n2)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(factoring,[status(thm)],[p7279]) ).
cnf(p7289,plain,
( ~ familiar(X0,n4)
| ~ familiar(n1,X0)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p7281,c39]) ).
cnf(p243,plain,
( ~ familiar(n6,n5)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p232,p207]) ).
cnf(p512,plain,
( ~ familiar(n6,n5)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p243]) ).
cnf(p123,plain,
( ~ not_familiar(n6,n5)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p112,p113]) ).
cnf(p548,plain,
( familiar(n1,n5)
| familiar(n1,n6)
| familiar(n6,n5) ),
inference(resolution,[status(thm)],[p250,p123]) ).
cnf(p1271,plain,
( familiar(n1,n5)
| familiar(n1,n6)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p512,p548]) ).
cnf(p4438,plain,
( familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p1271]) ).
cnf(p4441,plain,
( familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p4438]) ).
cnf(p7298,plain,
( familiar(n1,n5)
| familiar(n1,n2)
| ~ familiar(n6,n4)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p7289,p4441]) ).
cnf(p10562,plain,
( familiar(n1,n2)
| ~ familiar(n6,n4)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p7298]) ).
cnf(p10567,plain,
( ~ familiar(n6,n4)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p10562]) ).
cnf(p331,plain,
( ~ not_familiar(X0,n4)
| ~ not_familiar(n3,X0)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p179,c40]) ).
cnf(p396,plain,
( familiar(n3,n6)
| ~ not_familiar(n6,n4)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p331,p161]) ).
cnf(p515,plain,
( familiar(n6,n4)
| familiar(n3,n6)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p396,p236]) ).
cnf(p10569,plain,
( familiar(n3,n6)
| familiar(n4,n3)
| familiar(n1,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p10567,p515]) ).
cnf(p13716,plain,
( familiar(n3,n6)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p13709,p10569]) ).
cnf(p13900,plain,
( familiar(n3,n6)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p13716]) ).
cnf(p4443,plain,
( familiar(n6,n1)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4441,c37]) ).
cnf(p4449,plain,
( ~ familiar(X0,n6)
| ~ familiar(n1,X0)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p4443,c39]) ).
cnf(p12638,plain,
( ~ familiar(n3,n6)
| familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p12616,p4449]) ).
cnf(p12859,plain,
( ~ familiar(n3,n6)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p12638]) ).
cnf(p13911,plain,
( familiar(n1,n5)
| familiar(n1,n2)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p13900,p12859]) ).
cnf(p14119,plain,
( familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p13911]) ).
cnf(p14125,plain,
( familiar(n1,n5)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p14119]) ).
cnf(p13627,plain,
( familiar(n4,n1)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p13621,c37]) ).
cnf(p13672,plain,
( ~ familiar(X0,n4)
| ~ familiar(n1,X0)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p13627,c39]) ).
cnf(p14158,plain,
( ~ familiar(n5,n4)
| familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14125,p13672]) ).
cnf(p14210,plain,
( ~ familiar(n5,n4)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p14158]) ).
cnf(p395,plain,
( familiar(n3,n5)
| ~ not_familiar(n5,n4)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p331,p158]) ).
cnf(p514,plain,
( familiar(n5,n4)
| familiar(n3,n5)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p395,p214]) ).
cnf(p14211,plain,
( familiar(n3,n5)
| familiar(n4,n3)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14210,p514]) ).
cnf(p14313,plain,
( familiar(n1,n2)
| familiar(n3,n5)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14211,p13709]) ).
cnf(p14387,plain,
( familiar(n3,n5)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p14313]) ).
cnf(p14127,plain,
( familiar(n5,n1)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14125,c37]) ).
cnf(p14164,plain,
( ~ familiar(X0,n5)
| ~ familiar(n1,X0)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14127,c39]) ).
cnf(p14221,plain,
( familiar(n1,n2)
| ~ familiar(n3,n5)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14164,p12616]) ).
cnf(p14342,plain,
( ~ familiar(n3,n5)
| familiar(n1,n2) ),
inference(factoring,[status(thm)],[p14221]) ).
cnf(p14393,plain,
( familiar(n1,n2)
| familiar(n1,n2) ),
inference(resolution,[status(thm)],[p14387,p14342]) ).
cnf(p14404,plain,
familiar(n1,n2),
inference(factoring,[status(thm)],[p14393]) ).
cnf(p14419,plain,
( ~ familiar(n2,n5)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p14404,p7379]) ).
cnf(p15279,plain,
( familiar(n1,n3)
| familiar(n1,n4)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(resolution,[status(thm)],[p15271,p14419]) ).
cnf(p15297,plain,
( familiar(n1,n3)
| familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p15279]) ).
cnf(p15301,plain,
( familiar(n1,n3)
| familiar(n1,n4) ),
inference(factoring,[status(thm)],[p15297]) ).
cnf(p14406,plain,
familiar(n2,n1),
inference(resolution,[status(thm)],[p14404,c37]) ).
cnf(p14460,plain,
( ~ familiar(X0,n2)
| ~ familiar(n1,X0) ),
inference(resolution,[status(thm)],[p14406,c39]) ).
cnf(p15335,plain,
( ~ familiar(n4,n2)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p15301,p14460]) ).
cnf(p319,plain,
( ~ familiar(X0,n3)
| ~ familiar(n5,X0)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p290,c39]) ).
cnf(p720,plain,
( familiar(n1,n5)
| familiar(n4,n1)
| ~ familiar(n4,n3)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p319,p465]) ).
cnf(p1994,plain,
( familiar(n4,n1)
| ~ familiar(n4,n3)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p720]) ).
cnf(p391,plain,
( familiar(n1,n3)
| ~ not_familiar(n1,n4)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p331,p79]) ).
cnf(p700,plain,
( familiar(n1,n3)
| familiar(n4,n3)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p312,p391]) ).
cnf(p3652,plain,
( familiar(n1,n3)
| familiar(n4,n1)
| familiar(n4,n1)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p1994,p700]) ).
cnf(p7641,plain,
( familiar(n4,n1)
| familiar(n4,n1)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p3652]) ).
cnf(p7643,plain,
( familiar(n4,n1)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p7641]) ).
cnf(p7644,plain,
( ~ familiar(X0,n4)
| ~ familiar(n1,X0)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p7643,c39]) ).
cnf(p137,plain,
( familiar(n1,n5)
| ~ not_familiar(n5,n6)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p133,p106]) ).
cnf(p432,plain,
( familiar(n1,n5)
| familiar(n1,n6)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p219,p137]) ).
cnf(p718,plain,
( familiar(n1,n5)
| familiar(n1,n6)
| ~ familiar(n6,n3)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p319,p432]) ).
cnf(p1938,plain,
( familiar(n1,n6)
| ~ familiar(n6,n3)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p718]) ).
cnf(p3615,plain,
( familiar(n1,n3)
| familiar(n1,n6)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p1938,p339]) ).
cnf(p7511,plain,
( familiar(n1,n6)
| familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p3615]) ).
cnf(p7573,plain,
( familiar(n1,n6)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p7511]) ).
cnf(p7658,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| ~ familiar(n6,n4)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p7644,p7573]) ).
cnf(p11422,plain,
( familiar(n1,n3)
| ~ familiar(n6,n4)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p7658]) ).
cnf(p11424,plain,
( ~ familiar(n6,n4)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(factoring,[status(thm)],[p11422]) ).
cnf(p384,plain,
( familiar(n2,n6)
| ~ not_familiar(n6,n4)
| familiar(n4,n2) ),
inference(resolution,[status(thm)],[p325,p138]) ).
cnf(p504,plain,
( familiar(n6,n4)
| familiar(n2,n6)
| familiar(n4,n2) ),
inference(resolution,[status(thm)],[p384,p236]) ).
cnf(p11426,plain,
( familiar(n2,n6)
| familiar(n4,n2)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p11424,p504]) ).
cnf(p15360,plain,
( familiar(n2,n6)
| familiar(n1,n3)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p15335,p11426]) ).
cnf(p15707,plain,
( familiar(n2,n6)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p15360]) ).
cnf(p7575,plain,
( familiar(n6,n1)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p7573,c37]) ).
cnf(p7601,plain,
( ~ familiar(X0,n6)
| ~ familiar(n1,X0)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p7575,c39]) ).
cnf(p14421,plain,
( ~ familiar(n2,n6)
| familiar(n1,n3)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p14404,p7601]) ).
cnf(p15717,plain,
( familiar(n1,n3)
| familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p15707,p14421]) ).
cnf(p16018,plain,
( familiar(n1,n5)
| familiar(n1,n5)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p15717]) ).
cnf(p16020,plain,
( familiar(n1,n5)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p16018]) ).
cnf(p349,plain,
( ~ not_familiar(n5,n2)
| familiar(n2,n4)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p182,p150]) ).
cnf(p90,plain,
( ~ not_equal(n5,n2)
| not_familiar(n5,n2)
| familiar(n5,n2) ),
inference(resolution,[status(thm)],[p50,c1]) ).
cnf(f27,axiom,
not_equal(n5,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_5_2) ).
fof(f27_nnf,plain,
not_equal(n5,n2),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
not_equal(n5,n2),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(p202,plain,
( not_familiar(n5,n2)
| familiar(n5,n2) ),
inference(resolution,[status(thm)],[p90,c27]) ).
cnf(p442,plain,
( familiar(n5,n2)
| familiar(n2,n4)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p349,p202]) ).
cnf(p592,plain,
( ~ familiar(X0,n5)
| ~ familiar(n2,X0)
| familiar(n2,n4)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p442,c39]) ).
cnf(p14463,plain,
( ~ familiar(n1,n5)
| familiar(n2,n4)
| familiar(n4,n5) ),
inference(resolution,[status(thm)],[p14406,p592]) ).
cnf(p16042,plain,
( familiar(n2,n4)
| familiar(n4,n5)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p16020,p14463]) ).
cnf(p16087,plain,
( familiar(n5,n4)
| familiar(n2,n4)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p16042,c37]) ).
cnf(p15303,plain,
( familiar(n4,n1)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p15301,c37]) ).
cnf(p15343,plain,
( ~ familiar(X0,n4)
| ~ familiar(n1,X0)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p15303,c39]) ).
cnf(p16048,plain,
( ~ familiar(n5,n4)
| familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p16020,p15343]) ).
cnf(p16146,plain,
( ~ familiar(n5,n4)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p16048]) ).
cnf(p16187,plain,
( familiar(n1,n3)
| familiar(n2,n4)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p16087,p16146]) ).
cnf(p16249,plain,
( familiar(n2,n4)
| familiar(n1,n3) ),
inference(factoring,[status(thm)],[p16187]) ).
cnf(p15483,plain,
( ~ familiar(n2,n4)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p15343,p14404]) ).
cnf(p16257,plain,
( familiar(n1,n3)
| familiar(n1,n3) ),
inference(resolution,[status(thm)],[p16249,p15483]) ).
cnf(p16264,plain,
familiar(n1,n3),
inference(factoring,[status(thm)],[p16257]) ).
cnf(p277,plain,
( familiar(n2,n4)
| ~ not_familiar(n4,n3)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p267,p125]) ).
cnf(p337,plain,
( familiar(n2,n4)
| familiar(n3,n2)
| familiar(n4,n3) ),
inference(resolution,[status(thm)],[p179,p277]) ).
cnf(p418,plain,
( ~ familiar(X0,n4)
| ~ familiar(n3,X0)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p337,c39]) ).
cnf(p278,plain,
( familiar(n2,n5)
| ~ not_familiar(n5,n3)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p267,p132]) ).
cnf(p403,plain,
( familiar(n2,n5)
| familiar(n3,n2)
| familiar(n5,n3) ),
inference(resolution,[status(thm)],[p208,p278]) ).
cnf(p531,plain,
( familiar(n3,n5)
| familiar(n2,n5)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p403,c37]) ).
cnf(p987,plain,
( familiar(n2,n5)
| familiar(n3,n2)
| ~ familiar(n5,n4)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p418,p531]) ).
cnf(p3984,plain,
( familiar(n2,n5)
| ~ familiar(n5,n4)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(factoring,[status(thm)],[p987]) ).
cnf(p151,plain,
( not_familiar(n4,n2)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p125,c38]) ).
cnf(p285,plain,
( ~ not_familiar(X0,n4)
| ~ not_familiar(n2,X0)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p151,c40]) ).
cnf(p309,plain,
( familiar(n2,n5)
| ~ not_familiar(n5,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p285,p132]) ).
cnf(p417,plain,
( familiar(n2,n5)
| familiar(n2,n4)
| familiar(n5,n4) ),
inference(resolution,[status(thm)],[p214,p309]) ).
cnf(p3986,plain,
( familiar(n2,n5)
| familiar(n2,n4)
| familiar(n2,n5)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p3984,p417]) ).
cnf(p8065,plain,
( familiar(n2,n5)
| familiar(n2,n5)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(factoring,[status(thm)],[p3986]) ).
cnf(p8070,plain,
( familiar(n2,n5)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(factoring,[status(thm)],[p8065]) ).
cnf(p8071,plain,
( ~ familiar(X0,n3)
| ~ familiar(n2,X0)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p8070,c39]) ).
cnf(p14475,plain,
( ~ familiar(n1,n3)
| familiar(n2,n5)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p14406,p8071]) ).
cnf(p16296,plain,
( familiar(n2,n5)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16264,p14475]) ).
cnf(p16335,plain,
( familiar(n5,n2)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16296,c37]) ).
cnf(p16423,plain,
( ~ familiar(X0,n5)
| ~ familiar(n2,X0)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16335,c39]) ).
cnf(p295,plain,
( not_familiar(n6,n3)
| familiar(n3,n6) ),
inference(resolution,[status(thm)],[p161,c38]) ).
cnf(p279,plain,
( familiar(n2,n6)
| ~ not_familiar(n6,n3)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p267,p138]) ).
cnf(p649,plain,
( familiar(n2,n6)
| familiar(n3,n2)
| familiar(n3,n6) ),
inference(resolution,[status(thm)],[p295,p279]) ).
cnf(p989,plain,
( familiar(n2,n6)
| familiar(n3,n2)
| ~ familiar(n6,n4)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p418,p649]) ).
cnf(p4003,plain,
( familiar(n2,n6)
| ~ familiar(n6,n4)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(factoring,[status(thm)],[p989]) ).
cnf(p310,plain,
( familiar(n2,n6)
| ~ not_familiar(n6,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p285,p138]) ).
cnf(p499,plain,
( familiar(n2,n6)
| familiar(n2,n4)
| familiar(n6,n4) ),
inference(resolution,[status(thm)],[p236,p310]) ).
cnf(p4005,plain,
( familiar(n2,n6)
| familiar(n2,n4)
| familiar(n2,n6)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p4003,p499]) ).
cnf(p8099,plain,
( familiar(n2,n6)
| familiar(n2,n6)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(factoring,[status(thm)],[p4005]) ).
cnf(p8101,plain,
( familiar(n2,n6)
| familiar(n2,n4)
| familiar(n3,n2) ),
inference(factoring,[status(thm)],[p8099]) ).
cnf(p8102,plain,
( ~ familiar(X0,n3)
| ~ familiar(n2,X0)
| familiar(n2,n6)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p8101,c39]) ).
cnf(p14476,plain,
( ~ familiar(n1,n3)
| familiar(n2,n6)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p14406,p8102]) ).
cnf(p16297,plain,
( familiar(n2,n6)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16264,p14476]) ).
cnf(p16863,plain,
( familiar(n2,n4)
| ~ familiar(n6,n5)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16423,p16297]) ).
cnf(p16956,plain,
( ~ familiar(n6,n5)
| familiar(n2,n4) ),
inference(factoring,[status(thm)],[p16863]) ).
cnf(p89,plain,
( ~ not_equal(n5,n1)
| not_familiar(n5,n1)
| familiar(n5,n1) ),
inference(resolution,[status(thm)],[p50,c0]) ).
cnf(f26,axiom,
not_equal(n5,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_5_1) ).
fof(f26_nnf,plain,
not_equal(n5,n1),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
not_equal(n5,n1),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(p188,plain,
( not_familiar(n5,n1)
| familiar(n5,n1) ),
inference(resolution,[status(thm)],[p89,c26]) ).
cnf(p364,plain,
( not_familiar(n1,n5)
| familiar(n5,n1) ),
inference(resolution,[status(thm)],[p188,c38]) ).
cnf(p429,plain,
( ~ not_familiar(X0,n5)
| ~ not_familiar(n6,X0)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p219,c40]) ).
cnf(p98,plain,
( ~ not_equal(n6,n1)
| not_familiar(n6,n1)
| familiar(n6,n1) ),
inference(resolution,[status(thm)],[p51,c0]) ).
cnf(f31,axiom,
not_equal(n6,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_6_1) ).
fof(f31_nnf,plain,
not_equal(n6,n1),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
not_equal(n6,n1),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(p222,plain,
( not_familiar(n6,n1)
| familiar(n6,n1) ),
inference(resolution,[status(thm)],[p98,c31]) ).
cnf(p565,plain,
( familiar(n6,n1)
| ~ not_familiar(n1,n5)
| familiar(n5,n6) ),
inference(resolution,[status(thm)],[p429,p222]) ).
cnf(p863,plain,
( familiar(n6,n1)
| familiar(n5,n6)
| familiar(n5,n1) ),
inference(resolution,[status(thm)],[p364,p565]) ).
cnf(p1277,plain,
( ~ familiar(X0,n6)
| ~ familiar(n1,X0)
| familiar(n5,n6)
| familiar(n5,n1) ),
inference(resolution,[status(thm)],[p863,c39]) ).
cnf(p14418,plain,
( ~ familiar(n2,n6)
| familiar(n5,n6)
| familiar(n5,n1) ),
inference(resolution,[status(thm)],[p14404,p1277]) ).
cnf(p16396,plain,
( familiar(n5,n6)
| familiar(n5,n1)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16297,p14418]) ).
cnf(p16708,plain,
( familiar(n6,n5)
| familiar(n5,n1)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16396,c37]) ).
cnf(p16970,plain,
( familiar(n5,n1)
| familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16956,p16708]) ).
cnf(p17091,plain,
( familiar(n5,n1)
| familiar(n2,n4) ),
inference(factoring,[status(thm)],[p16970]) ).
cnf(p14405,plain,
( ~ familiar(X0,n1)
| ~ familiar(n2,X0) ),
inference(resolution,[status(thm)],[p14404,c39]) ).
cnf(p16356,plain,
( ~ familiar(n5,n1)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p16296,p14405]) ).
cnf(p17095,plain,
( familiar(n2,n4)
| familiar(n2,n4) ),
inference(resolution,[status(thm)],[p17091,p16356]) ).
cnf(p17098,plain,
familiar(n2,n4),
inference(factoring,[status(thm)],[p17095]) ).
cnf(p584,plain,
( ~ familiar(X0,n5)
| ~ familiar(n6,X0)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p432,c39]) ).
cnf(p361,plain,
( familiar(n1,n6)
| ~ not_familiar(n6,n4)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p311,p112]) ).
cnf(p500,plain,
( familiar(n1,n6)
| familiar(n4,n1)
| familiar(n6,n4) ),
inference(resolution,[status(thm)],[p236,p361]) ).
cnf(p1491,plain,
( familiar(n1,n6)
| familiar(n4,n1)
| ~ familiar(n4,n5)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p584,p500]) ).
cnf(p4844,plain,
( familiar(n4,n1)
| ~ familiar(n4,n5)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p1491]) ).
cnf(p641,plain,
( familiar(n4,n5)
| familiar(n1,n5)
| familiar(n4,n1) ),
inference(resolution,[status(thm)],[p465,c37]) ).
cnf(p4847,plain,
( familiar(n1,n5)
| familiar(n4,n1)
| familiar(n4,n1)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p4844,p641]) ).
cnf(p8908,plain,
( familiar(n4,n1)
| familiar(n4,n1)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p4847]) ).
cnf(p8910,plain,
( familiar(n4,n1)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(factoring,[status(thm)],[p8908]) ).
cnf(p8911,plain,
( ~ familiar(X0,n4)
| ~ familiar(n1,X0)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p8910,c39]) ).
cnf(p14430,plain,
( ~ familiar(n2,n4)
| familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p14404,p8911]) ).
cnf(p17130,plain,
( familiar(n1,n5)
| familiar(n1,n6) ),
inference(resolution,[status(thm)],[p17098,p14430]) ).
cnf(p16266,plain,
familiar(n3,n1),
inference(resolution,[status(thm)],[p16264,c37]) ).
cnf(p100,plain,
( ~ not_equal(n6,n3)
| not_familiar(n6,n3)
| familiar(n6,n3) ),
inference(resolution,[status(thm)],[p51,c2]) ).
cnf(f33,axiom,
not_equal(n6,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_equal_6_3) ).
fof(f33_nnf,plain,
not_equal(n6,n3),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
not_equal(n6,n3),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(p228,plain,
( not_familiar(n6,n3)
| familiar(n6,n3) ),
inference(resolution,[status(thm)],[p100,c33]) ).
cnf(p472,plain,
( familiar(n2,n6)
| familiar(n3,n2)
| familiar(n6,n3) ),
inference(resolution,[status(thm)],[p228,p279]) ).
cnf(p669,plain,
( ~ familiar(X0,n6)
| ~ familiar(n3,X0)
| familiar(n2,n6)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p472,c39]) ).
cnf(p16307,plain,
( ~ familiar(n1,n6)
| familiar(n2,n6)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p16266,p669]) ).
cnf(p17179,plain,
( familiar(n2,n6)
| familiar(n3,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p17130,p16307]) ).
cnf(p16295,plain,
~ familiar(n3,n2),
inference(resolution,[status(thm)],[p16264,p14460]) ).
cnf(p17498,plain,
( familiar(n2,n6)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p17179,p16295]) ).
cnf(p17500,plain,
( familiar(n6,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p17498,c37]) ).
cnf(p17173,plain,
( ~ familiar(n6,n2)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p17130,p14460]) ).
cnf(p17528,plain,
( familiar(n1,n5)
| familiar(n1,n5) ),
inference(resolution,[status(thm)],[p17500,p17173]) ).
cnf(p17529,plain,
familiar(n1,n5),
inference(factoring,[status(thm)],[p17528]) ).
cnf(p530,plain,
( ~ familiar(X0,n5)
| ~ familiar(n3,X0)
| familiar(n2,n5)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p403,c39]) ).
cnf(p16304,plain,
( ~ familiar(n1,n5)
| familiar(n2,n5)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p16266,p530]) ).
cnf(p17551,plain,
( familiar(n2,n5)
| familiar(n3,n2) ),
inference(resolution,[status(thm)],[p17529,p16304]) ).
cnf(p17663,plain,
familiar(n2,n5),
inference(resolution,[status(thm)],[p17551,p16295]) ).
cnf(p17665,plain,
familiar(n5,n2),
inference(resolution,[status(thm)],[p17663,c37]) ).
cnf(p17544,plain,
~ familiar(n5,n2),
inference(resolution,[status(thm)],[p17529,p14460]) ).
cnf(p17683,plain,
$false,
inference(resolution,[status(thm)],[p17665,p17544]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ028-6 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.58 % Computer : n011.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Thu Sep 24 06:41:28 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.58 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 58.97/27.49 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/27.49 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------