%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO579+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:20 EDT 2024
% Result : Theorem 7.13s 7.32s
% Output : Refutation 7.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 4
% Syntax : Number of formulae : 49 ( 27 unt; 0 def)
% Number of atoms : 115 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 88 ( 22 ~; 17 |; 44 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-8 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 75 ( 1 sgn 44 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(exemplo6GDDFULL416041,conjecture,
! [A,B,C,I,Y,L,X] :
( ( eqangle(I,A,A,B,I,A,A,C)
& eqangle(I,B,B,C,I,B,B,A)
& eqangle(I,C,C,A,I,C,C,B)
& perp(Y,I,A,C)
& coll(Y,A,C)
& perp(L,I,B,C)
& coll(L,B,C)
& perp(X,B,A,I)
& coll(X,A,I) )
=> coll(X,Y,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL416041) ).
fof(c11,negated_conjecture,
~ ! [A,B,C,I,Y,L,X] :
( ( eqangle(I,A,A,B,I,A,A,C)
& eqangle(I,B,B,C,I,B,B,A)
& eqangle(I,C,C,A,I,C,C,B)
& perp(Y,I,A,C)
& coll(Y,A,C)
& perp(L,I,B,C)
& coll(L,B,C)
& perp(X,B,A,I)
& coll(X,A,I) )
=> coll(X,Y,L) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL416041]) ).
fof(c12,negated_conjecture,
? [A,B,C,I,Y,L,X] :
( eqangle(I,A,A,B,I,A,A,C)
& eqangle(I,B,B,C,I,B,B,A)
& eqangle(I,C,C,A,I,C,C,B)
& perp(Y,I,A,C)
& coll(Y,A,C)
& perp(L,I,B,C)
& coll(L,B,C)
& perp(X,B,A,I)
& coll(X,A,I)
& ~ coll(X,Y,L) ),
inference(fof_nnf,[status(thm)],[c11]) ).
fof(c13,negated_conjecture,
? [X2,X3,X4,X5,X6,X7,X8] :
( 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,X5,X2,X4)
& coll(X6,X2,X4)
& perp(X7,X5,X3,X4)
& coll(X7,X3,X4)
& perp(X8,X3,X2,X5)
& coll(X8,X2,X5)
& ~ coll(X8,X6,X7) ),
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,skolem0004,skolem0001,skolem0003)
& coll(skolem0005,skolem0001,skolem0003)
& perp(skolem0006,skolem0004,skolem0002,skolem0003)
& coll(skolem0006,skolem0002,skolem0003)
& perp(skolem0007,skolem0002,skolem0001,skolem0004)
& coll(skolem0007,skolem0001,skolem0004)
& ~ coll(skolem0007,skolem0005,skolem0006) ),
inference(skolemize,[status(esa)],[c13]) ).
cnf(c24,negated_conjecture,
~ coll(skolem0007,skolem0005,skolem0006),
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(c404,plain,
! [A,B,C] :
( ~ coll(A,B,C)
| coll(B,A,C) ),
inference(fof_nnf,[status(thm)],[ruleD2]) ).
fof(c405,plain,
! [X524,X525,X526] :
( ~ coll(X524,X525,X526)
| coll(X525,X524,X526) ),
inference(variable_rename,[status(thm)],[c404]) ).
cnf(c406,plain,
( ~ coll(X552,X554,X553)
| coll(X554,X552,X553) ),
inference(split_conjunct,[status(thm)],[c405]) ).
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,
! [X527,X528,X529] :
( ~ coll(X527,X528,X529)
| coll(X527,X529,X528) ),
inference(variable_rename,[status(thm)],[c407]) ).
cnf(c409,plain,
( ~ coll(X571,X572,X573)
| coll(X571,X573,X572) ),
inference(split_conjunct,[status(thm)],[c408]) ).
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,
! [X520,X521,X522,X523] :
( ~ coll(X520,X521,X522)
| ~ coll(X520,X521,X523)
| coll(X522,X523,X520) ),
inference(variable_rename,[status(thm)],[c401]) ).
cnf(c403,plain,
( ~ coll(X743,X744,X741)
| ~ coll(X743,X744,X742)
| coll(X741,X742,X743) ),
inference(split_conjunct,[status(thm)],[c402]) ).
cnf(c543,plain,
( ~ coll(X747,X745,X746)
| coll(X746,X746,X747) ),
inference(factor,[status(thm)],[c403]) ).
cnf(c23,negated_conjecture,
coll(skolem0007,skolem0001,skolem0004),
inference(split_conjunct,[status(thm)],[c14]) ).
cnf(c431,plain,
coll(skolem0007,skolem0004,skolem0001),
inference(resolution,[status(thm)],[c409,c23]) ).
cnf(c570,plain,
coll(skolem0001,skolem0001,skolem0007),
inference(resolution,[status(thm)],[c543,c431]) ).
cnf(c19,negated_conjecture,
coll(skolem0005,skolem0001,skolem0003),
inference(split_conjunct,[status(thm)],[c14]) ).
cnf(c432,plain,
coll(skolem0005,skolem0003,skolem0001),
inference(resolution,[status(thm)],[c409,c19]) ).
cnf(c447,plain,
coll(skolem0003,skolem0005,skolem0001),
inference(resolution,[status(thm)],[c432,c406]) ).
cnf(c565,plain,
coll(skolem0001,skolem0001,skolem0003),
inference(resolution,[status(thm)],[c543,c447]) ).
cnf(c596,plain,
( ~ coll(skolem0001,skolem0001,X1065)
| coll(X1065,skolem0003,skolem0001) ),
inference(resolution,[status(thm)],[c565,c403]) ).
cnf(c1174,plain,
coll(skolem0007,skolem0003,skolem0001),
inference(resolution,[status(thm)],[c596,c570]) ).
cnf(c1180,plain,
coll(skolem0007,skolem0001,skolem0003),
inference(resolution,[status(thm)],[c1174,c409]) ).
cnf(c1195,plain,
coll(skolem0003,skolem0003,skolem0007),
inference(resolution,[status(thm)],[c1180,c543]) ).
cnf(c21,negated_conjecture,
coll(skolem0006,skolem0002,skolem0003),
inference(split_conjunct,[status(thm)],[c14]) ).
cnf(c579,plain,
coll(skolem0003,skolem0003,skolem0006),
inference(resolution,[status(thm)],[c543,c21]) ).
cnf(c668,plain,
( ~ coll(skolem0003,skolem0003,X1537)
| coll(X1537,skolem0006,skolem0003) ),
inference(resolution,[status(thm)],[c579,c403]) ).
cnf(c2333,plain,
coll(skolem0007,skolem0006,skolem0003),
inference(resolution,[status(thm)],[c668,c1195]) ).
cnf(c2439,plain,
coll(skolem0007,skolem0003,skolem0006),
inference(resolution,[status(thm)],[c2333,c409]) ).
cnf(c418,plain,
coll(skolem0001,skolem0005,skolem0003),
inference(resolution,[status(thm)],[c406,c19]) ).
cnf(c428,plain,
coll(skolem0001,skolem0003,skolem0005),
inference(resolution,[status(thm)],[c409,c418]) ).
cnf(c435,plain,
coll(skolem0003,skolem0001,skolem0005),
inference(resolution,[status(thm)],[c428,c406]) ).
cnf(c559,plain,
( ~ coll(skolem0003,skolem0001,X1035)
| coll(X1035,skolem0005,skolem0003) ),
inference(resolution,[status(thm)],[c403,c435]) ).
cnf(c1182,plain,
coll(skolem0003,skolem0007,skolem0001),
inference(resolution,[status(thm)],[c1174,c406]) ).
cnf(c1199,plain,
coll(skolem0003,skolem0001,skolem0007),
inference(resolution,[status(thm)],[c1182,c409]) ).
cnf(c1237,plain,
coll(skolem0007,skolem0005,skolem0003),
inference(resolution,[status(thm)],[c1199,c559]) ).
cnf(c1298,plain,
coll(skolem0007,skolem0003,skolem0005),
inference(resolution,[status(thm)],[c1237,c409]) ).
cnf(c1359,plain,
( ~ coll(skolem0007,skolem0003,X1911)
| coll(X1911,skolem0005,skolem0007) ),
inference(resolution,[status(thm)],[c1298,c403]) ).
cnf(c4145,plain,
coll(skolem0006,skolem0005,skolem0007),
inference(resolution,[status(thm)],[c1359,c2439]) ).
cnf(c4163,plain,
coll(skolem0005,skolem0006,skolem0007),
inference(resolution,[status(thm)],[c4145,c406]) ).
cnf(c4193,plain,
coll(skolem0005,skolem0007,skolem0006),
inference(resolution,[status(thm)],[c4163,c409]) ).
cnf(c4233,plain,
coll(skolem0007,skolem0005,skolem0006),
inference(resolution,[status(thm)],[c4193,c406]) ).
cnf(c4276,plain,
$false,
inference(resolution,[status(thm)],[c4233,c24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO579+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n016.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 9 08:10:37 EDT 2024
% 0.13/0.33 % CPUTime :
% 7.13/7.32 % Version: 1.5
% 7.13/7.32 % SZS status Theorem
% 7.13/7.32 % SZS output start CNFRefutation
% See solution above
% 7.13/7.32
% 7.13/7.32 % Initial clauses : 137
% 7.13/7.32 % Processed clauses : 846
% 7.13/7.32 % Factors computed : 59
% 7.13/7.32 % Resolvents computed: 3816
% 7.13/7.32 % Tautologies deleted: 4
% 7.13/7.32 % Forward subsumed : 1437
% 7.13/7.32 % Backward subsumed : 0
% 7.13/7.32 % -------- CPU Time ---------
% 7.13/7.32 % User time : 6.956 s
% 7.13/7.32 % System time : 0.021 s
% 7.13/7.32 % Total time : 6.977 s
%------------------------------------------------------------------------------