%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GEO255+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Sun Sep 27 07:14:59 AM UTC 2026
% Result : Theorem 20.93s 3.21s
% Output : CNFRefutation 20.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO255+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n018.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Fri Sep 25 13:13:05 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.93/3.21 % SZS status Theorem for theBenchmark.p
% 20.93/3.21 % SZS output start CNFRefutation for theBenchmark.p
% 20.93/3.21 fof(a4_defns, axiom, ! [X0] : ! [X1] : (('equally$udirected$ulines'(X0,X1) <=> ~'unequally$udirected$ulines'(X0,X1)))).
% 20.93/3.21 fof(ax4_defns, axiom, ! [X0] : ! [X1] : ! [X2] : (('before$uon$uline'(X0,X1,X2) <=> ('distinct$upoints'(X1,X2) & ('incident$upoint$uand$uline'(X1,X0) & ('incident$upoint$uand$uline'(X2,X0) & 'equally$udirected$ulines'(X0,'line$uconnecting'(X1,X2)))))))).
% 20.93/3.21 fof(ax5_basics, axiom, ! [X0] : 'equally$udirected$ulines'(X0,X0)).
% 20.93/3.21 fof(ax6_basics, axiom, ! [X0] : ! [X1] : ! [X2] : (('unequally$udirected$ulines'(X0,X1) => ('unequally$udirected$ulines'(X0,X2) | 'unequally$udirected$ulines'(X1,X2))))).
% 20.93/3.21 fof(ax8_basics, axiom, ! [X0] : ! [X1] : (('unequally$udirected$ulines'(X0,X1) | 'unequally$udirected$ulines'(X0,'reverse$uline'(X1))))).
% 20.93/3.21 fof(ax9_basics, axiom, ! [X0] : ! [X1] : ((('unequally$udirected$ulines'(X0,X1) & 'unequally$udirected$ulines'(X0,'reverse$uline'(X1))) => ('left$uconvergent$ulines'(X0,X1) | 'left$uconvergent$ulines'(X0,'reverse$uline'(X1)))))).
% 20.93/3.21 fof(ax11_basics, axiom, ! [X0] : ! [X1] : ~(('left$uconvergent$ulines'(X0,X1) | 'left$uconvergent$ulines'(X0,'reverse$uline'(X1))))).
% 20.93/3.21 fof(ax9_cons_objs, axiom, ! [X0] : ! [X1] : (('distinct$upoints'(X0,X1) => 'equally$udirected$ulines'('line$uconnecting'(X0,X1),'reverse$uline'('line$uconnecting'(X1,X0)))))).
% 20.93/3.21 fof(con, conjecture, ! [X0] : ! [X1] : ! [X2] : ~(('before$uon$uline'(X0,X1,X2) & 'before$uon$uline'(X0,X2,X1)))).
% 20.93/3.21 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ~(('before$uon$uline'(X0,X1,X2) & 'before$uon$uline'(X0,X2,X1))), inference(negate_conjecture, [status(cth)], [con])).
% 20.93/3.21 cnf(c6, plain, ~'equally$udirected$ulines'(X0,X1) | ~'unequally$udirected$ulines'(X0,X1), inference(clausification, [status(esa)], [a4_defns])).
% 20.93/3.21 cnf(c24, plain, ~'before$uon$uline'(X0,X1,X2) | X3(X1,X2,X0), inference(clausification, [status(esa)], [ax4_defns])).
% 20.93/3.21 cnf(c26, plain, ~X0(X1,X2,X3) | 'distinct$upoints'(X1,X2), inference(clausification, [status(esa)], [ax4_defns])).
% 20.93/3.21 cnf(c29, plain, ~X0(X1,X2,X3) | 'equally$udirected$ulines'(X3,'line$uconnecting'(X1,X2)), inference(clausification, [status(esa)], [ax4_defns])).
% 20.93/3.21 cnf(c43, plain, 'equally$udirected$ulines'(X0,X0), inference(clausification, [status(esa)], [ax5_basics])).
% 20.93/3.21 cnf(c44, plain, ~'unequally$udirected$ulines'(X0,X1) | 'unequally$udirected$ulines'(X0,X2) | 'unequally$udirected$ulines'(X1,X2), inference(clausification, [status(esa)], [ax6_basics])).
% 20.93/3.21 cnf(c49, plain, 'unequally$udirected$ulines'(X0,X1) | 'unequally$udirected$ulines'(X0,'reverse$uline'(X1)), inference(clausification, [status(esa)], [ax8_basics])).
% 20.93/3.21 cnf(c50, plain, ~'unequally$udirected$ulines'(X0,X1) | ~'unequally$udirected$ulines'(X0,'reverse$uline'(X1)) | 'left$uconvergent$ulines'(X0,X1) | 'left$uconvergent$ulines'(X0,'reverse$uline'(X1)), inference(clausification, [status(esa)], [ax9_basics])).
% 20.93/3.21 cnf(c53, plain, ~'left$uconvergent$ulines'(X0,X1), inference(clausification, [status(esa)], [ax11_basics])).
% 20.93/3.21 cnf(c65, plain, ~'distinct$upoints'(X0,X1) | 'equally$udirected$ulines'('line$uconnecting'(X0,X1),'reverse$uline'('line$uconnecting'(X1,X0))), inference(clausification, [status(esa)], [ax9_cons_objs])).
% 20.93/3.21 cnf(c72, plain, 'before$uon$uline'(sK84,sK85,sK86), inference(clausification, [status(esa)], [negated_conjecture])).
% 20.93/3.21 cnf(c73, plain, 'before$uon$uline'(sK84,sK86,sK85), inference(clausification, [status(esa)], [negated_conjecture])).
% 20.93/3.21 cnf(d0, plain, ~'Ts18'(X0,X1,X2) | ~'unequally$udirected$ulines'(X2,'line$uconnecting'(X0,X1)), inference(resolution, [status(thm)], [c29,c6])).
% 20.93/3.21 cnf(d1, plain, ~'distinct$upoints'(X0,X1) | ~'unequally$udirected$ulines'('line$uconnecting'(X0,X1),'reverse$uline'('line$uconnecting'(X1,X0))), inference(resolution, [status(thm)], [c65,c6])).
% 20.93/3.21 cnf(d2, plain, ~'unequally$udirected$ulines'(X0,X1) | ~'unequally$udirected$ulines'(X0,'reverse$uline'(X1)) | 'left$uconvergent$ulines'(X0,'reverse$uline'(X1)), inference(resolution, [status(thm)], [c53,c50])).
% 20.93/3.21 cnf(d3, plain, ~'unequally$udirected$ulines'(X0,X0), inference(resolution, [status(thm)], [c6,c43])).
% 20.93/3.21 cnf(d4, plain, 'unequally$udirected$ulines'('reverse$uline'(X0),X0), inference(resolution, [status(thm)], [c49,d3])).
% 20.93/3.21 cnf(d5, plain, 'unequally$udirected$ulines'(X0,X1) | 'unequally$udirected$ulines'('reverse$uline'(X0),X1), inference(resolution, [status(thm)], [c44,d4])).
% 20.93/3.21 cnf(d6, plain, 'unequally$udirected$ulines'(X0,'reverse$uline'(X1)) | ~'unequally$udirected$ulines'('reverse$uline'(X0),X1) | 'left$uconvergent$ulines'('reverse$uline'(X0),'reverse$uline'(X1)), inference(resolution, [status(thm)], [d5,d2])).
% 20.93/3.21 cnf(d7, plain, 'unequally$udirected$ulines'(X0,'reverse$uline'(X1)) | ~'unequally$udirected$ulines'('reverse$uline'(X0),X1), inference(resolution, [status(thm)], [c53,d6])).
% 20.93/3.21 cnf(d8, plain, 'Ts18'(sK85,sK86,sK84), inference(resolution, [status(thm)], [c24,c72])).
% 20.93/3.21 cnf(d9, plain, 'unequally$udirected$ulines'('reverse$uline'(X0),X1) | 'unequally$udirected$ulines'(X2,X1) | 'unequally$udirected$ulines'(X2,X0), inference(resolution, [status(thm)], [c44,c49])).
% 20.93/3.21 cnf(d10, plain, 'unequally$udirected$ulines'(X0,X1) | 'unequally$udirected$ulines'('reverse$uline'(X1),'line$uconnecting'(X2,X3)) | ~'Ts18'(X2,X3,X0), inference(resolution, [status(thm)], [d9,d0])).
% 20.93/3.21 cnf(d11, plain, 'unequally$udirected$ulines'(sK84,X0) | 'unequally$udirected$ulines'('reverse$uline'(X0),'line$uconnecting'(sK85,sK86)), inference(resolution, [status(thm)], [d10,d8])).
% 20.93/3.21 cnf(d12, plain, 'unequally$udirected$ulines'(sK84,X0) | 'unequally$udirected$ulines'(X0,'reverse$uline'('line$uconnecting'(sK85,sK86))), inference(resolution, [status(thm)], [d11,d7])).
% 20.93/3.21 cnf(d13, plain, 'unequally$udirected$ulines'(sK84,'line$uconnecting'(sK86,sK85)) | ~'distinct$upoints'(sK86,sK85), inference(resolution, [status(thm)], [d12,d1])).
% 20.93/3.21 cnf(d14, plain, 'Ts18'(sK86,sK85,sK84), inference(resolution, [status(thm)], [c24,c73])).
% 20.93/3.21 cnf(d15, plain, 'distinct$upoints'(sK86,sK85), inference(resolution, [status(thm)], [d14,c26])).
% 20.93/3.21 cnf(d16, plain, 'unequally$udirected$ulines'(sK84,'line$uconnecting'(sK86,sK85)), inference(resolution, [status(thm)], [d15,d13])).
% 20.93/3.21 cnf(d17, plain, ~'Ts18'(sK86,sK85,sK84), inference(resolution, [status(thm)], [d16,d0])).
% 20.93/3.21 cnf(d18, plain, $false, inference(resolution, [status(thm)], [d14,d17])).
% 20.93/3.21 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------