%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO547+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:22:15 EDT 2024
% Result : Theorem 3.65s 3.84s
% Output : Refutation 3.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 4
% Syntax : Number of formulae : 53 ( 29 unt; 0 def)
% Number of atoms : 123 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 94 ( 24 ~; 18 |; 47 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 93 ( 1 sgn 48 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(exemplo6GDDFULL012007,conjecture,
! [A,B,C,O,D,E,F,G,NWPNT1] :
( ( circle(O,A,B,C)
& circle(O,A,D,NWPNT1)
& perp(E,D,B,C)
& coll(E,B,C)
& perp(F,D,A,C)
& coll(F,A,C)
& perp(G,D,A,B)
& coll(G,A,B) )
=> coll(E,F,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL012007) ).
fof(c11,negated_conjecture,
~ ! [A,B,C,O,D,E,F,G,NWPNT1] :
( ( circle(O,A,B,C)
& circle(O,A,D,NWPNT1)
& perp(E,D,B,C)
& coll(E,B,C)
& perp(F,D,A,C)
& coll(F,A,C)
& perp(G,D,A,B)
& coll(G,A,B) )
=> coll(E,F,G) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL012007]) ).
fof(c12,negated_conjecture,
? [A,B,C,O,D,E,F,G,NWPNT1] :
( circle(O,A,B,C)
& circle(O,A,D,NWPNT1)
& perp(E,D,B,C)
& coll(E,B,C)
& perp(F,D,A,C)
& coll(F,A,C)
& perp(G,D,A,B)
& coll(G,A,B)
& ~ coll(E,F,G) ),
inference(fof_nnf,[status(thm)],[c11]) ).
fof(c13,negated_conjecture,
? [A,B,C,O,D,E,F,G] :
( circle(O,A,B,C)
& ? [NWPNT1] : circle(O,A,D,NWPNT1)
& perp(E,D,B,C)
& coll(E,B,C)
& perp(F,D,A,C)
& coll(F,A,C)
& perp(G,D,A,B)
& coll(G,A,B)
& ~ coll(E,F,G) ),
inference(shift_quantors,[status(thm)],[c12]) ).
fof(c14,negated_conjecture,
? [X2,X3,X4,X5,X6,X7,X8,X9] :
( circle(X5,X2,X3,X4)
& ? [X10] : circle(X5,X2,X6,X10)
& perp(X7,X6,X3,X4)
& coll(X7,X3,X4)
& perp(X8,X6,X2,X4)
& coll(X8,X2,X4)
& perp(X9,X6,X2,X3)
& coll(X9,X2,X3)
& ~ coll(X7,X8,X9) ),
inference(variable_rename,[status(thm)],[c13]) ).
fof(c15,negated_conjecture,
( circle(skolem0004,skolem0001,skolem0002,skolem0003)
& circle(skolem0004,skolem0001,skolem0005,skolem0009)
& perp(skolem0006,skolem0005,skolem0002,skolem0003)
& coll(skolem0006,skolem0002,skolem0003)
& perp(skolem0007,skolem0005,skolem0001,skolem0003)
& coll(skolem0007,skolem0001,skolem0003)
& perp(skolem0008,skolem0005,skolem0001,skolem0002)
& coll(skolem0008,skolem0001,skolem0002)
& ~ coll(skolem0006,skolem0007,skolem0008) ),
inference(skolemize,[status(esa)],[c14]) ).
cnf(c24,negated_conjecture,
~ coll(skolem0006,skolem0007,skolem0008),
inference(split_conjunct,[status(thm)],[c15]) ).
fof(ruleD1,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(A,C,B) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(c407,plain,
! [A,B,C] :
( ~ coll(A,B,C)
| coll(A,C,B) ),
inference(fof_nnf,[status(thm)],[ruleD1]) ).
fof(c408,plain,
! [X529,X530,X531] :
( ~ coll(X529,X530,X531)
| coll(X529,X531,X530) ),
inference(variable_rename,[status(thm)],[c407]) ).
cnf(c409,plain,
( ~ coll(X573,X574,X575)
| coll(X573,X575,X574) ),
inference(split_conjunct,[status(thm)],[c408]) ).
fof(ruleD2,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(B,A,C) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD2) ).
fof(c404,plain,
! [A,B,C] :
( ~ coll(A,B,C)
| coll(B,A,C) ),
inference(fof_nnf,[status(thm)],[ruleD2]) ).
fof(c405,plain,
! [X526,X527,X528] :
( ~ coll(X526,X527,X528)
| coll(X527,X526,X528) ),
inference(variable_rename,[status(thm)],[c404]) ).
cnf(c406,plain,
( ~ coll(X562,X564,X563)
| coll(X564,X562,X563) ),
inference(split_conjunct,[status(thm)],[c405]) ).
cnf(c23,negated_conjecture,
coll(skolem0008,skolem0001,skolem0002),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c418,plain,
coll(skolem0001,skolem0008,skolem0002),
inference(resolution,[status(thm)],[c406,c23]) ).
cnf(c431,plain,
coll(skolem0001,skolem0002,skolem0008),
inference(resolution,[status(thm)],[c409,c418]) ).
fof(ruleD3,axiom,
! [A,B,C,D] :
( ( coll(A,B,C)
& coll(A,B,D) )
=> coll(C,D,A) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD3) ).
fof(c401,plain,
! [A,B,C,D] :
( ~ coll(A,B,C)
| ~ coll(A,B,D)
| coll(C,D,A) ),
inference(fof_nnf,[status(thm)],[ruleD3]) ).
fof(c402,plain,
! [X522,X523,X524,X525] :
( ~ coll(X522,X523,X524)
| ~ coll(X522,X523,X525)
| coll(X524,X525,X522) ),
inference(variable_rename,[status(thm)],[c401]) ).
cnf(c403,plain,
( ~ coll(X761,X760,X758)
| ~ coll(X761,X760,X759)
| coll(X758,X759,X761) ),
inference(split_conjunct,[status(thm)],[c402]) ).
cnf(c551,plain,
( ~ coll(skolem0001,skolem0002,X1010)
| coll(X1010,skolem0008,skolem0001) ),
inference(resolution,[status(thm)],[c403,c431]) ).
cnf(c19,negated_conjecture,
coll(skolem0006,skolem0002,skolem0003),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c417,plain,
coll(skolem0002,skolem0006,skolem0003),
inference(resolution,[status(thm)],[c406,c19]) ).
cnf(c428,plain,
coll(skolem0002,skolem0003,skolem0006),
inference(resolution,[status(thm)],[c409,c417]) ).
cnf(c548,plain,
( ~ coll(skolem0002,skolem0003,X999)
| coll(X999,skolem0006,skolem0002) ),
inference(resolution,[status(thm)],[c403,c428]) ).
cnf(c21,negated_conjecture,
coll(skolem0007,skolem0001,skolem0003),
inference(split_conjunct,[status(thm)],[c15]) ).
cnf(c416,plain,
coll(skolem0001,skolem0007,skolem0003),
inference(resolution,[status(thm)],[c406,c21]) ).
cnf(c552,plain,
( ~ coll(skolem0001,skolem0007,X1015)
| coll(X1015,skolem0003,skolem0001) ),
inference(resolution,[status(thm)],[c403,c416]) ).
cnf(c432,plain,
coll(skolem0008,skolem0002,skolem0001),
inference(resolution,[status(thm)],[c409,c23]) ).
cnf(c446,plain,
coll(skolem0002,skolem0008,skolem0001),
inference(resolution,[status(thm)],[c432,c406]) ).
cnf(c543,plain,
( ~ coll(X768,X769,X770)
| coll(X770,X770,X768) ),
inference(factor,[status(thm)],[c403]) ).
cnf(c576,plain,
coll(skolem0001,skolem0001,skolem0002),
inference(resolution,[status(thm)],[c543,c446]) ).
cnf(c429,plain,
coll(skolem0007,skolem0003,skolem0001),
inference(resolution,[status(thm)],[c409,c21]) ).
cnf(c563,plain,
coll(skolem0001,skolem0001,skolem0007),
inference(resolution,[status(thm)],[c543,c429]) ).
cnf(c584,plain,
( ~ coll(skolem0001,skolem0001,X1064)
| coll(X1064,skolem0007,skolem0001) ),
inference(resolution,[status(thm)],[c563,c403]) ).
cnf(c1158,plain,
coll(skolem0002,skolem0007,skolem0001),
inference(resolution,[status(thm)],[c584,c576]) ).
cnf(c1163,plain,
coll(skolem0007,skolem0002,skolem0001),
inference(resolution,[status(thm)],[c1158,c406]) ).
cnf(c1178,plain,
coll(skolem0007,skolem0001,skolem0002),
inference(resolution,[status(thm)],[c1163,c409]) ).
cnf(c1201,plain,
coll(skolem0001,skolem0007,skolem0002),
inference(resolution,[status(thm)],[c1178,c406]) ).
cnf(c1257,plain,
coll(skolem0002,skolem0003,skolem0001),
inference(resolution,[status(thm)],[c1201,c552]) ).
cnf(c1323,plain,
coll(skolem0001,skolem0006,skolem0002),
inference(resolution,[status(thm)],[c1257,c548]) ).
cnf(c1418,plain,
coll(skolem0001,skolem0002,skolem0006),
inference(resolution,[status(thm)],[c1323,c409]) ).
cnf(c1537,plain,
coll(skolem0006,skolem0008,skolem0001),
inference(resolution,[status(thm)],[c1418,c551]) ).
cnf(c1719,plain,
coll(skolem0008,skolem0006,skolem0001),
inference(resolution,[status(thm)],[c1537,c406]) ).
cnf(c1866,plain,
coll(skolem0008,skolem0001,skolem0006),
inference(resolution,[status(thm)],[c1719,c409]) ).
cnf(c578,plain,
coll(skolem0001,skolem0001,skolem0008),
inference(resolution,[status(thm)],[c543,c432]) ).
cnf(c1160,plain,
coll(skolem0008,skolem0007,skolem0001),
inference(resolution,[status(thm)],[c584,c578]) ).
cnf(c1172,plain,
coll(skolem0008,skolem0001,skolem0007),
inference(resolution,[status(thm)],[c1160,c409]) ).
cnf(c1195,plain,
( ~ coll(skolem0008,skolem0001,X1603)
| coll(X1603,skolem0007,skolem0008) ),
inference(resolution,[status(thm)],[c1172,c403]) ).
cnf(c2560,plain,
coll(skolem0006,skolem0007,skolem0008),
inference(resolution,[status(thm)],[c1195,c1866]) ).
cnf(c2568,plain,
$false,
inference(resolution,[status(thm)],[c2560,c24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : GEO547+1 : TPTP v8.1.2. Released v7.5.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Thu May 9 08:06:53 EDT 2024
% 0.15/0.37 % CPUTime :
% 3.65/3.84 % Version: 1.5
% 3.65/3.84 % SZS status Theorem
% 3.65/3.84 % SZS output start CNFRefutation
% See solution above
% 3.65/3.84
% 3.65/3.84 % Initial clauses : 136
% 3.65/3.84 % Processed clauses : 587
% 3.65/3.84 % Factors computed : 38
% 3.65/3.84 % Resolvents computed: 2123
% 3.65/3.84 % Tautologies deleted: 4
% 3.65/3.84 % Forward subsumed : 954
% 3.65/3.84 % Backward subsumed : 0
% 3.65/3.84 % -------- CPU Time ---------
% 3.65/3.84 % User time : 3.453 s
% 3.65/3.84 % System time : 0.015 s
% 3.65/3.84 % Total time : 3.468 s
%------------------------------------------------------------------------------