%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV399+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:44:54 EDT 2024
% Result : Theorem 2.76s 2.98s
% Output : Refutation 2.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV399+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n025.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 06:12:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 2.76/2.98 % Version: 1.5
% 2.76/2.98 % SZS status Theorem
% 2.76/2.98 % SZS output start CNFRefutation
% 2.76/2.98 fof(l35_co,conjecture,(![U]:((?[V]:(?[W]:(pair_in_list(U,V,W)&strictly_less_than(V,W))))=>(![X]:(?[Y]:(?[Z]:(pair_in_list(update_slb(U,X),Y,Z)&strictly_less_than(Y,Z))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l35_co)).
% 2.76/2.98 fof(c10,negated_conjecture,(~(![U]:((?[V]:(?[W]:(pair_in_list(U,V,W)&strictly_less_than(V,W))))=>(![X]:(?[Y]:(?[Z]:(pair_in_list(update_slb(U,X),Y,Z)&strictly_less_than(Y,Z)))))))),inference(assume_negation,[status(cth)],[l35_co])).
% 2.76/2.98 fof(c11,negated_conjecture,(?[U]:((?[V]:(?[W]:(pair_in_list(U,V,W)&strictly_less_than(V,W))))&(?[X]:(![Y]:(![Z]:(~pair_in_list(update_slb(U,X),Y,Z)|~strictly_less_than(Y,Z))))))),inference(fof_nnf,[status(thm)],[c10])).
% 2.76/2.98 fof(c12,negated_conjecture,(?[X2]:((?[X3]:(?[X4]:(pair_in_list(X2,X3,X4)&strictly_less_than(X3,X4))))&(?[X5]:(![X6]:(![X7]:(~pair_in_list(update_slb(X2,X5),X6,X7)|~strictly_less_than(X6,X7))))))),inference(variable_rename,[status(thm)],[c11])).
% 2.76/2.98 fof(c14,negated_conjecture,(![X6]:(![X7]:((pair_in_list(skolem0001,skolem0002,skolem0003)&strictly_less_than(skolem0002,skolem0003))&(~pair_in_list(update_slb(skolem0001,skolem0004),X6,X7)|~strictly_less_than(X6,X7))))),inference(shift_quantors,[status(thm)],[fof(c13,negated_conjecture,((pair_in_list(skolem0001,skolem0002,skolem0003)&strictly_less_than(skolem0002,skolem0003))&(![X6]:(![X7]:(~pair_in_list(update_slb(skolem0001,skolem0004),X6,X7)|~strictly_less_than(X6,X7))))),inference(skolemize,[status(esa)],[c12])).])).
% 2.76/2.98 cnf(c16,negated_conjecture,strictly_less_than(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 2.76/2.98 cnf(c17,negated_conjecture,~pair_in_list(update_slb(skolem0001,skolem0004),X195,X194)|~strictly_less_than(X195,X194),inference(split_conjunct,[status(thm)],[c14])).
% 2.76/2.98 cnf(c15,negated_conjecture,pair_in_list(skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 2.76/2.98 fof(l35_li3637,plain,(![U]:(![V]:(![W]:(![X]:((pair_in_list(U,V,W)&less_than(X,W))=>pair_in_list(update_slb(U,X),V,W)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l35_li3637)).
% 2.76/2.98 fof(c21,plain,(![U]:(![V]:(![W]:(![X]:((~pair_in_list(U,V,W)|~less_than(X,W))|pair_in_list(update_slb(U,X),V,W)))))),inference(fof_nnf,[status(thm)],[l35_li3637])).
% 2.76/2.98 fof(c22,plain,(![X12]:(![X13]:(![X14]:(![X15]:((~pair_in_list(X12,X13,X14)|~less_than(X15,X14))|pair_in_list(update_slb(X12,X15),X13,X14)))))),inference(variable_rename,[status(thm)],[c21])).
% 2.76/2.98 cnf(c23,plain,~pair_in_list(X208,X206,X209)|~less_than(X207,X209)|pair_in_list(update_slb(X208,X207),X206,X209),inference(split_conjunct,[status(thm)],[c22])).
% 2.76/2.98 cnf(c200,plain,~less_than(X817,skolem0003)|pair_in_list(update_slb(skolem0001,X817),skolem0002,skolem0003),inference(resolution,[status(thm)],[c23, c15])).
% 2.76/2.98 fof(totality,axiom,(![U]:(![V]:(less_than(U,V)|less_than(V,U)))),file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax', totality)).
% 2.76/2.98 fof(c86,plain,(![X69]:(![X70]:(less_than(X69,X70)|less_than(X70,X69)))),inference(variable_rename,[status(thm)],[totality])).
% 2.76/2.98 cnf(c87,plain,less_than(X96,X97)|less_than(X97,X96),inference(split_conjunct,[status(thm)],[c86])).
% 2.76/2.98 fof(stricly_smaller_definition,axiom,(![U]:(![V]:(strictly_less_than(U,V)<=>(less_than(U,V)&(~less_than(V,U)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax', stricly_smaller_definition)).
% 2.76/2.98 fof(c75,plain,(![U]:(![V]:(strictly_less_than(U,V)<=>(less_than(U,V)&~less_than(V,U))))),inference(fof_simplification,[status(thm)],[stricly_smaller_definition])).
% 2.76/2.98 fof(c76,plain,(![U]:(![V]:((~strictly_less_than(U,V)|(less_than(U,V)&~less_than(V,U)))&((~less_than(U,V)|less_than(V,U))|strictly_less_than(U,V))))),inference(fof_nnf,[status(thm)],[c75])).
% 2.76/2.98 fof(c77,plain,((![U]:(![V]:(~strictly_less_than(U,V)|(less_than(U,V)&~less_than(V,U)))))&(![U]:(![V]:((~less_than(U,V)|less_than(V,U))|strictly_less_than(U,V))))),inference(shift_quantors,[status(thm)],[c76])).
% 2.76/2.98 fof(c79,plain,(![X64]:(![X65]:(![X66]:(![X67]:((~strictly_less_than(X64,X65)|(less_than(X64,X65)&~less_than(X65,X64)))&((~less_than(X66,X67)|less_than(X67,X66))|strictly_less_than(X66,X67))))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,((![X64]:(![X65]:(~strictly_less_than(X64,X65)|(less_than(X64,X65)&~less_than(X65,X64)))))&(![X66]:(![X67]:((~less_than(X66,X67)|less_than(X67,X66))|strictly_less_than(X66,X67))))),inference(variable_rename,[status(thm)],[c77])).])).
% 2.76/2.98 fof(c80,plain,(![X64]:(![X65]:(![X66]:(![X67]:(((~strictly_less_than(X64,X65)|less_than(X64,X65))&(~strictly_less_than(X64,X65)|~less_than(X65,X64)))&((~less_than(X66,X67)|less_than(X67,X66))|strictly_less_than(X66,X67))))))),inference(distribute,[status(thm)],[c79])).
% 2.76/2.98 cnf(c83,plain,~less_than(X125,X126)|less_than(X126,X125)|strictly_less_than(X125,X126),inference(split_conjunct,[status(thm)],[c80])).
% 2.76/2.98 cnf(c120,plain,less_than(X132,X131)|strictly_less_than(X131,X132),inference(resolution,[status(thm)],[c83, c87])).
% 2.76/2.98 cnf(c81,plain,~strictly_less_than(X83,X84)|less_than(X83,X84),inference(split_conjunct,[status(thm)],[c80])).
% 2.76/2.98 cnf(c92,plain,less_than(skolem0002,skolem0003),inference(resolution,[status(thm)],[c81, c16])).
% 2.76/2.98 fof(transitivity,axiom,(![U]:(![V]:(![W]:((less_than(U,V)&less_than(V,W))=>less_than(U,W))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax', transitivity)).
% 2.76/2.98 fof(c88,plain,(![U]:(![V]:(![W]:((~less_than(U,V)|~less_than(V,W))|less_than(U,W))))),inference(fof_nnf,[status(thm)],[transitivity])).
% 2.76/2.98 fof(c89,plain,(![X71]:(![X72]:(![X73]:((~less_than(X71,X72)|~less_than(X72,X73))|less_than(X71,X73))))),inference(variable_rename,[status(thm)],[c88])).
% 2.76/2.98 cnf(c90,plain,~less_than(X147,X148)|~less_than(X148,X149)|less_than(X147,X149),inference(split_conjunct,[status(thm)],[c89])).
% 2.76/2.98 cnf(c143,plain,~less_than(X193,skolem0002)|less_than(X193,skolem0003),inference(resolution,[status(thm)],[c90, c92])).
% 2.76/2.98 cnf(c177,plain,less_than(X203,skolem0003)|strictly_less_than(skolem0002,X203),inference(resolution,[status(thm)],[c143, c120])).
% 2.76/2.98 fof(l35_li3839,plain,(![U]:(![V]:(![W]:(![X]:((pair_in_list(U,V,W)&strictly_less_than(W,X))=>pair_in_list(update_slb(U,X),V,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l35_li3839)).
% 2.76/2.98 fof(c18,plain,(![U]:(![V]:(![W]:(![X]:((~pair_in_list(U,V,W)|~strictly_less_than(W,X))|pair_in_list(update_slb(U,X),V,X)))))),inference(fof_nnf,[status(thm)],[l35_li3839])).
% 2.76/2.98 fof(c19,plain,(![X8]:(![X9]:(![X10]:(![X11]:((~pair_in_list(X8,X9,X10)|~strictly_less_than(X10,X11))|pair_in_list(update_slb(X8,X11),X9,X11)))))),inference(variable_rename,[status(thm)],[c18])).
% 2.76/2.98 cnf(c20,plain,~pair_in_list(X201,X199,X200)|~strictly_less_than(X200,X202)|pair_in_list(update_slb(X201,X202),X199,X202),inference(split_conjunct,[status(thm)],[c19])).
% 2.76/2.98 cnf(c187,plain,~strictly_less_than(skolem0003,X770)|pair_in_list(update_slb(skolem0001,X770),skolem0002,X770),inference(resolution,[status(thm)],[c20, c15])).
% 2.76/2.98 cnf(c1232,plain,pair_in_list(update_slb(skolem0001,X2031),skolem0002,X2031)|less_than(X2031,skolem0003),inference(resolution,[status(thm)],[c187, c120])).
% 2.76/2.98 cnf(c8732,plain,less_than(skolem0004,skolem0003)|~strictly_less_than(skolem0002,skolem0004),inference(resolution,[status(thm)],[c1232, c17])).
% 2.76/2.98 cnf(c8763,plain,less_than(skolem0004,skolem0003),inference(resolution,[status(thm)],[c8732, c177])).
% 2.76/2.98 cnf(c8784,plain,pair_in_list(update_slb(skolem0001,skolem0004),skolem0002,skolem0003),inference(resolution,[status(thm)],[c8763, c200])).
% 2.76/2.98 cnf(c9467,plain,~strictly_less_than(skolem0002,skolem0003),inference(resolution,[status(thm)],[c8784, c17])).
% 2.76/2.98 cnf(c9491,plain,$false,inference(resolution,[status(thm)],[c9467, c16])).
% 2.76/2.98 % SZS output end CNFRefutation
% 2.76/2.98
% 2.76/2.98 % Initial clauses : 43
% 2.76/2.98 % Processed clauses : 357
% 2.76/2.98 % Factors computed : 70
% 2.76/2.98 % Resolvents computed: 9351
% 2.76/2.98 % Tautologies deleted: 6
% 2.76/2.98 % Forward subsumed : 677
% 2.76/2.98 % Backward subsumed : 5
% 2.76/2.98 % -------- CPU Time ---------
% 2.76/2.98 % User time : 2.598 s
% 2.76/2.98 % System time : 0.028 s
% 2.76/2.98 % Total time : 2.626 s
%------------------------------------------------------------------------------