%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWC291+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:43:47 EDT 2024
% Result : Theorem 0.56s 0.76s
% Output : Refutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SWC291+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.32 % Computer : n032.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu May 9 03:13:07 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.56/0.76 % Version: 1.5
% 0.56/0.76 % SZS status Theorem
% 0.56/0.76 % SZS output start CNFRefutation
% 0.56/0.76 fof(co1,conjecture,(![U]:(ssList(U)=>(![V]:(ssList(V)=>(![W]:(ssList(W)=>(![X]:(ssList(X)=>(((((V!=X|U!=W)|(~segmentP(X,W)))|(~strictorderedP(W)))|(?[Y]:((((ssList(Y)&neq(W,Y))&segmentP(X,Y))&segmentP(Y,W))&strictorderedP(Y))))|strictorderedP(U)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.56/0.76 fof(c23,negated_conjecture,(~(![U]:(ssList(U)=>(![V]:(ssList(V)=>(![W]:(ssList(W)=>(![X]:(ssList(X)=>(((((V!=X|U!=W)|(~segmentP(X,W)))|(~strictorderedP(W)))|(?[Y]:((((ssList(Y)&neq(W,Y))&segmentP(X,Y))&segmentP(Y,W))&strictorderedP(Y))))|strictorderedP(U))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.56/0.76 fof(c24,negated_conjecture,(~(![U]:(ssList(U)=>(![V]:(ssList(V)=>(![W]:(ssList(W)=>(![X]:(ssList(X)=>(((((V!=X|U!=W)|~segmentP(X,W))|~strictorderedP(W))|(?[Y]:((((ssList(Y)&neq(W,Y))&segmentP(X,Y))&segmentP(Y,W))&strictorderedP(Y))))|strictorderedP(U))))))))))),inference(fof_simplification,[status(thm)],[c23])).
% 0.56/0.76 fof(c25,negated_conjecture,(?[U]:(ssList(U)&(?[V]:(ssList(V)&(?[W]:(ssList(W)&(?[X]:(ssList(X)&(((((V=X&U=W)&segmentP(X,W))&strictorderedP(W))&(![Y]:((((~ssList(Y)|~neq(W,Y))|~segmentP(X,Y))|~segmentP(Y,W))|~strictorderedP(Y))))&~strictorderedP(U)))))))))),inference(fof_nnf,[status(thm)],[c24])).
% 0.56/0.76 fof(c26,negated_conjecture,(?[X2]:(ssList(X2)&(?[X3]:(ssList(X3)&(?[X4]:(ssList(X4)&(?[X5]:(ssList(X5)&(((((X3=X5&X2=X4)&segmentP(X5,X4))&strictorderedP(X4))&(![X6]:((((~ssList(X6)|~neq(X4,X6))|~segmentP(X5,X6))|~segmentP(X6,X4))|~strictorderedP(X6))))&~strictorderedP(X2)))))))))),inference(variable_rename,[status(thm)],[c25])).
% 0.56/0.76 fof(c28,negated_conjecture,(![X6]:(ssList(skolem0001)&(ssList(skolem0002)&(ssList(skolem0003)&(ssList(skolem0004)&(((((skolem0002=skolem0004&skolem0001=skolem0003)&segmentP(skolem0004,skolem0003))&strictorderedP(skolem0003))&((((~ssList(X6)|~neq(skolem0003,X6))|~segmentP(skolem0004,X6))|~segmentP(X6,skolem0003))|~strictorderedP(X6)))&~strictorderedP(skolem0001))))))),inference(shift_quantors,[status(thm)],[fof(c27,negated_conjecture,(ssList(skolem0001)&(ssList(skolem0002)&(ssList(skolem0003)&(ssList(skolem0004)&(((((skolem0002=skolem0004&skolem0001=skolem0003)&segmentP(skolem0004,skolem0003))&strictorderedP(skolem0003))&(![X6]:((((~ssList(X6)|~neq(skolem0003,X6))|~segmentP(skolem0004,X6))|~segmentP(X6,skolem0003))|~strictorderedP(X6))))&~strictorderedP(skolem0001)))))),inference(skolemize,[status(esa)],[c26])).])).
% 0.56/0.76 cnf(c38,negated_conjecture,~strictorderedP(skolem0001),inference(split_conjunct,[status(thm)],[c28])).
% 0.56/0.76 cnf(c36,negated_conjecture,strictorderedP(skolem0003),inference(split_conjunct,[status(thm)],[c28])).
% 0.56/0.76 cnf(symmetry,axiom,X253!=X252|X252=X253,theory(equality)).
% 0.56/0.76 cnf(c34,negated_conjecture,skolem0001=skolem0003,inference(split_conjunct,[status(thm)],[c28])).
% 0.56/0.76 cnf(c520,plain,skolem0003=skolem0001,inference(resolution,[status(thm)],[c34, symmetry])).
% 0.56/0.76 cnf(c18,axiom,X334!=X335|~strictorderedP(X334)|strictorderedP(X335),theory(equality)).
% 0.56/0.76 cnf(c643,plain,~strictorderedP(skolem0003)|strictorderedP(skolem0001),inference(resolution,[status(thm)],[c18, c520])).
% 0.56/0.76 cnf(c650,plain,strictorderedP(skolem0001),inference(resolution,[status(thm)],[c643, c36])).
% 0.56/0.76 cnf(c656,plain,$false,inference(resolution,[status(thm)],[c650, c38])).
% 0.56/0.76 % SZS output end CNFRefutation
% 0.56/0.76
% 0.56/0.76 % Initial clauses : 226
% 0.56/0.76 % Processed clauses : 115
% 0.56/0.76 % Factors computed : 3
% 0.56/0.76 % Resolvents computed: 146
% 0.56/0.76 % Tautologies deleted: 11
% 0.56/0.76 % Forward subsumed : 13
% 0.56/0.76 % Backward subsumed : 1
% 0.56/0.76 % -------- CPU Time ---------
% 0.56/0.76 % User time : 0.425 s
% 0.56/0.76 % System time : 0.010 s
% 0.56/0.76 % Total time : 0.435 s
%------------------------------------------------------------------------------