%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO620+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:25 EDT 2024
% Result : Theorem 7.51s 7.71s
% Output : Refutation 7.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 4
% Syntax : Number of formulae : 60 ( 36 unt; 0 def)
% Number of atoms : 133 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 97 ( 24 ~; 19 |; 49 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-8 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 81 ( 1 sgn 46 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(exemplo6GDDFULL8110982,conjecture,
! [A,B,C,O,I,E,J,L] :
( ( eqangle(O,A,A,B,O,A,A,C)
& eqangle(O,B,B,C,O,B,B,A)
& eqangle(O,C,C,A,O,C,C,B)
& perp(I,C,A,O)
& coll(I,A,O)
& perp(A,O,A,E)
& perp(J,C,A,E)
& coll(J,A,E)
& perp(L,C,B,O)
& coll(L,B,O) )
=> coll(I,L,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL8110982) ).
fof(c11,negated_conjecture,
~ ! [A,B,C,O,I,E,J,L] :
( ( eqangle(O,A,A,B,O,A,A,C)
& eqangle(O,B,B,C,O,B,B,A)
& eqangle(O,C,C,A,O,C,C,B)
& perp(I,C,A,O)
& coll(I,A,O)
& perp(A,O,A,E)
& perp(J,C,A,E)
& coll(J,A,E)
& perp(L,C,B,O)
& coll(L,B,O) )
=> coll(I,L,J) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110982]) ).
fof(c12,negated_conjecture,
? [A,B,C,O,I,E,J,L] :
( eqangle(O,A,A,B,O,A,A,C)
& eqangle(O,B,B,C,O,B,B,A)
& eqangle(O,C,C,A,O,C,C,B)
& perp(I,C,A,O)
& coll(I,A,O)
& perp(A,O,A,E)
& perp(J,C,A,E)
& coll(J,A,E)
& perp(L,C,B,O)
& coll(L,B,O)
& ~ coll(I,L,J) ),
inference(fof_nnf,[status(thm)],[c11]) ).
fof(c13,negated_conjecture,
? [X2,X3,X4,X5,X6,X7,X8,X9] :
( eqangle(X5,X2,X2,X3,X5,X2,X2,X4)
& eqangle(X5,X3,X3,X4,X5,X3,X3,X2)
& eqangle(X5,X4,X4,X2,X5,X4,X4,X3)
& perp(X6,X4,X2,X5)
& coll(X6,X2,X5)
& perp(X2,X5,X2,X7)
& perp(X8,X4,X2,X7)
& coll(X8,X2,X7)
& perp(X9,X4,X3,X5)
& coll(X9,X3,X5)
& ~ coll(X6,X9,X8) ),
inference(variable_rename,[status(thm)],[c12]) ).
fof(c14,negated_conjecture,
( eqangle(skolem0004,skolem0001,skolem0001,skolem0002,skolem0004,skolem0001,skolem0001,skolem0003)
& eqangle(skolem0004,skolem0002,skolem0002,skolem0003,skolem0004,skolem0002,skolem0002,skolem0001)
& eqangle(skolem0004,skolem0003,skolem0003,skolem0001,skolem0004,skolem0003,skolem0003,skolem0002)
& perp(skolem0005,skolem0003,skolem0001,skolem0004)
& coll(skolem0005,skolem0001,skolem0004)
& perp(skolem0001,skolem0004,skolem0001,skolem0006)
& perp(skolem0007,skolem0003,skolem0001,skolem0006)
& coll(skolem0007,skolem0001,skolem0006)
& perp(skolem0008,skolem0003,skolem0002,skolem0004)
& coll(skolem0008,skolem0002,skolem0004)
& ~ coll(skolem0005,skolem0008,skolem0007) ),
inference(skolemize,[status(esa)],[c13]) ).
cnf(c25,negated_conjecture,
~ coll(skolem0005,skolem0008,skolem0007),
inference(split_conjunct,[status(thm)],[c14]) ).
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(c405,plain,
! [A,B,C] :
( ~ coll(A,B,C)
| coll(B,A,C) ),
inference(fof_nnf,[status(thm)],[ruleD2]) ).
fof(c406,plain,
! [X525,X526,X527] :
( ~ coll(X525,X526,X527)
| coll(X526,X525,X527) ),
inference(variable_rename,[status(thm)],[c405]) ).
cnf(c407,plain,
( ~ coll(X561,X563,X562)
| coll(X563,X561,X562) ),
inference(split_conjunct,[status(thm)],[c406]) ).
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(c408,plain,
! [A,B,C] :
( ~ coll(A,B,C)
| coll(A,C,B) ),
inference(fof_nnf,[status(thm)],[ruleD1]) ).
fof(c409,plain,
! [X528,X529,X530] :
( ~ coll(X528,X529,X530)
| coll(X528,X530,X529) ),
inference(variable_rename,[status(thm)],[c408]) ).
cnf(c410,plain,
( ~ coll(X574,X573,X572)
| coll(X574,X572,X573) ),
inference(split_conjunct,[status(thm)],[c409]) ).
cnf(c19,negated_conjecture,
coll(skolem0005,skolem0001,skolem0004),
inference(split_conjunct,[status(thm)],[c14]) ).
cnf(c419,plain,
coll(skolem0001,skolem0005,skolem0004),
inference(resolution,[status(thm)],[c407,c19]) ).
cnf(c431,plain,
coll(skolem0001,skolem0004,skolem0005),
inference(resolution,[status(thm)],[c410,c419]) ).
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(c402,plain,
! [A,B,C,D] :
( ~ coll(A,B,C)
| ~ coll(A,B,D)
| coll(C,D,A) ),
inference(fof_nnf,[status(thm)],[ruleD3]) ).
fof(c403,plain,
! [X521,X522,X523,X524] :
( ~ coll(X521,X522,X523)
| ~ coll(X521,X522,X524)
| coll(X523,X524,X521) ),
inference(variable_rename,[status(thm)],[c402]) ).
cnf(c404,plain,
( ~ coll(X757,X759,X758)
| ~ coll(X757,X759,X760)
| coll(X758,X760,X757) ),
inference(split_conjunct,[status(thm)],[c403]) ).
cnf(c596,plain,
( ~ coll(skolem0001,skolem0004,X1053)
| coll(X1053,skolem0005,skolem0001) ),
inference(resolution,[status(thm)],[c404,c431]) ).
cnf(c24,negated_conjecture,
coll(skolem0008,skolem0002,skolem0004),
inference(split_conjunct,[status(thm)],[c14]) ).
cnf(c579,plain,
( ~ coll(X769,X768,X767)
| coll(X767,X767,X769) ),
inference(factor,[status(thm)],[c404]) ).
cnf(c604,plain,
coll(skolem0004,skolem0004,skolem0008),
inference(resolution,[status(thm)],[c579,c24]) ).
cnf(c603,plain,
coll(skolem0004,skolem0004,skolem0001),
inference(resolution,[status(thm)],[c579,c419]) ).
cnf(c640,plain,
( ~ coll(skolem0004,skolem0004,X1364)
| coll(X1364,skolem0001,skolem0004) ),
inference(resolution,[status(thm)],[c603,c404]) ).
cnf(c1840,plain,
coll(skolem0008,skolem0001,skolem0004),
inference(resolution,[status(thm)],[c640,c604]) ).
cnf(c1852,plain,
coll(skolem0001,skolem0008,skolem0004),
inference(resolution,[status(thm)],[c1840,c407]) ).
cnf(c1878,plain,
coll(skolem0001,skolem0004,skolem0008),
inference(resolution,[status(thm)],[c1852,c410]) ).
cnf(c1936,plain,
coll(skolem0008,skolem0005,skolem0001),
inference(resolution,[status(thm)],[c1878,c596]) ).
cnf(c2022,plain,
coll(skolem0005,skolem0008,skolem0001),
inference(resolution,[status(thm)],[c1936,c407]) ).
cnf(c2126,plain,
coll(skolem0005,skolem0001,skolem0008),
inference(resolution,[status(thm)],[c2022,c410]) ).
cnf(c435,plain,
coll(skolem0005,skolem0004,skolem0001),
inference(resolution,[status(thm)],[c410,c19]) ).
cnf(c616,plain,
coll(skolem0001,skolem0001,skolem0005),
inference(resolution,[status(thm)],[c579,c435]) ).
cnf(c22,negated_conjecture,
coll(skolem0007,skolem0001,skolem0006),
inference(split_conjunct,[status(thm)],[c14]) ).
cnf(c434,plain,
coll(skolem0007,skolem0006,skolem0001),
inference(resolution,[status(thm)],[c410,c22]) ).
cnf(c450,plain,
coll(skolem0006,skolem0007,skolem0001),
inference(resolution,[status(thm)],[c434,c407]) ).
cnf(c599,plain,
coll(skolem0001,skolem0001,skolem0006),
inference(resolution,[status(thm)],[c579,c450]) ).
cnf(c619,plain,
( ~ coll(skolem0001,skolem0001,X1069)
| coll(X1069,skolem0006,skolem0001) ),
inference(resolution,[status(thm)],[c599,c404]) ).
cnf(c1252,plain,
coll(skolem0005,skolem0006,skolem0001),
inference(resolution,[status(thm)],[c619,c616]) ).
cnf(c1260,plain,
coll(skolem0005,skolem0001,skolem0006),
inference(resolution,[status(thm)],[c1252,c410]) ).
cnf(c1280,plain,
( ~ coll(skolem0005,skolem0001,X1668)
| coll(X1668,skolem0006,skolem0005) ),
inference(resolution,[status(thm)],[c1260,c404]) ).
cnf(c3594,plain,
coll(skolem0008,skolem0006,skolem0005),
inference(resolution,[status(thm)],[c1280,c2126]) ).
cnf(c3601,plain,
coll(skolem0006,skolem0008,skolem0005),
inference(resolution,[status(thm)],[c3594,c407]) ).
cnf(c3616,plain,
coll(skolem0006,skolem0005,skolem0008),
inference(resolution,[status(thm)],[c3601,c410]) ).
cnf(c3641,plain,
coll(skolem0005,skolem0006,skolem0008),
inference(resolution,[status(thm)],[c3616,c407]) ).
cnf(c417,plain,
coll(skolem0001,skolem0007,skolem0006),
inference(resolution,[status(thm)],[c407,c22]) ).
cnf(c430,plain,
coll(skolem0001,skolem0006,skolem0007),
inference(resolution,[status(thm)],[c410,c417]) ).
cnf(c438,plain,
coll(skolem0006,skolem0001,skolem0007),
inference(resolution,[status(thm)],[c430,c407]) ).
cnf(c593,plain,
( ~ coll(skolem0006,skolem0001,X1042)
| coll(X1042,skolem0007,skolem0006) ),
inference(resolution,[status(thm)],[c404,c438]) ).
cnf(c1262,plain,
coll(skolem0006,skolem0005,skolem0001),
inference(resolution,[status(thm)],[c1252,c407]) ).
cnf(c1286,plain,
coll(skolem0006,skolem0001,skolem0005),
inference(resolution,[status(thm)],[c1262,c410]) ).
cnf(c1341,plain,
coll(skolem0005,skolem0007,skolem0006),
inference(resolution,[status(thm)],[c1286,c593]) ).
cnf(c1402,plain,
coll(skolem0005,skolem0006,skolem0007),
inference(resolution,[status(thm)],[c1341,c410]) ).
cnf(c1472,plain,
( ~ coll(skolem0005,skolem0006,X1866)
| coll(X1866,skolem0007,skolem0005) ),
inference(resolution,[status(thm)],[c1402,c404]) ).
cnf(c4430,plain,
coll(skolem0008,skolem0007,skolem0005),
inference(resolution,[status(thm)],[c1472,c3641]) ).
cnf(c4438,plain,
coll(skolem0008,skolem0005,skolem0007),
inference(resolution,[status(thm)],[c4430,c410]) ).
cnf(c4472,plain,
coll(skolem0005,skolem0008,skolem0007),
inference(resolution,[status(thm)],[c4438,c407]) ).
cnf(c4512,plain,
$false,
inference(resolution,[status(thm)],[c4472,c25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO620+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 07:43:23 EDT 2024
% 0.14/0.34 % CPUTime :
% 7.51/7.71 % Version: 1.5
% 7.51/7.71 % SZS status Theorem
% 7.51/7.71 % SZS output start CNFRefutation
% See solution above
% 7.51/7.71
% 7.51/7.71 % Initial clauses : 138
% 7.51/7.71 % Processed clauses : 883
% 7.51/7.71 % Factors computed : 53
% 7.51/7.71 % Resolvents computed: 4049
% 7.51/7.71 % Tautologies deleted: 4
% 7.51/7.71 % Forward subsumed : 1511
% 7.51/7.71 % Backward subsumed : 0
% 7.51/7.71 % -------- CPU Time ---------
% 7.51/7.71 % User time : 7.341 s
% 7.51/7.71 % System time : 0.019 s
% 7.51/7.71 % Total time : 7.360 s
%------------------------------------------------------------------------------