%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : RNG124+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:38:25 EDT 2024
% Result : Theorem 65.69s 65.93s
% Output : Refutation 65.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : RNG124+4 : TPTP v8.1.2. Released v4.0.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n022.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Wed May 8 21:15:38 EDT 2024
% 0.14/0.37 % CPUTime :
% 65.69/65.93 % Version: 1.5
% 65.69/65.93 % SZS status Theorem
% 65.69/65.93 % SZS output start CNFRefutation
% 65.69/65.93 fof(m__2673,plain,xr!=sz00,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2673)).
% 65.69/65.93 cnf(c41,plain,xr!=sz00,inference(split_conjunct,[status(thm)],[m__2673])).
% 65.69/65.93 fof(m__2729,plain,((?[W0]:(?[W1]:((aElementOf0(W0,slsdtgt0(xa))&aElementOf0(W1,slsdtgt0(xb)))&sdtpldt0(W0,W1)=xr)))&aElementOf0(xr,xI)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2729)).
% 65.69/65.93 fof(c21,plain,((?[X2]:(?[X3]:((aElementOf0(X2,slsdtgt0(xa))&aElementOf0(X3,slsdtgt0(xb)))&sdtpldt0(X2,X3)=xr)))&aElementOf0(xr,xI)),inference(variable_rename,[status(thm)],[m__2729])).
% 65.69/65.93 fof(c22,plain,(((aElementOf0(skolem0001,slsdtgt0(xa))&aElementOf0(skolem0002,slsdtgt0(xb)))&sdtpldt0(skolem0001,skolem0002)=xr)&aElementOf0(xr,xI)),inference(skolemize,[status(esa)],[c21])).
% 65.69/65.93 cnf(c26,plain,aElementOf0(xr,xI),inference(split_conjunct,[status(thm)],[c22])).
% 65.69/65.93 fof(m__2666,plain,(((aElement0(xq)&aElement0(xr))&xb=sdtpldt0(sdtasdt0(xq,xu),xr))&(xr=sz00|iLess0(sbrdtbr0(xr),sbrdtbr0(xu)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2666)).
% 65.69/65.93 cnf(c45,plain,xr=sz00|iLess0(sbrdtbr0(xr),sbrdtbr0(xu)),inference(split_conjunct,[status(thm)],[m__2666])).
% 65.69/65.93 fof(m__2273,plain,((((?[W0]:(?[W1]:((aElementOf0(W0,slsdtgt0(xa))&aElementOf0(W1,slsdtgt0(xb)))&sdtpldt0(W0,W1)=xu)))&aElementOf0(xu,xI))&xu!=sz00)&(![W0]:((((?[W1]:(?[W2]:((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))|aElementOf0(W0,xI))&W0!=sz00)=>(~iLess0(sbrdtbr0(W0),sbrdtbr0(xu)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2273)).
% 65.69/65.93 fof(c75,plain,((((?[W0]:(?[W1]:((aElementOf0(W0,slsdtgt0(xa))&aElementOf0(W1,slsdtgt0(xb)))&sdtpldt0(W0,W1)=xu)))&aElementOf0(xu,xI))&xu!=sz00)&(![W0]:((((?[W1]:(?[W2]:((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))|aElementOf0(W0,xI))&W0!=sz00)=>~iLess0(sbrdtbr0(W0),sbrdtbr0(xu))))),inference(fof_simplification,[status(thm)],[m__2273])).
% 65.69/65.93 fof(c76,plain,((((?[W0]:(?[W1]:((aElementOf0(W0,slsdtgt0(xa))&aElementOf0(W1,slsdtgt0(xb)))&sdtpldt0(W0,W1)=xu)))&aElementOf0(xu,xI))&xu!=sz00)&(![W0]:((((![W1]:(![W2]:((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|sdtpldt0(W1,W2)!=W0)))&~aElementOf0(W0,xI))|W0=sz00)|~iLess0(sbrdtbr0(W0),sbrdtbr0(xu))))),inference(fof_nnf,[status(thm)],[c75])).
% 65.69/65.93 fof(c77,plain,((((?[X14]:(?[X15]:((aElementOf0(X14,slsdtgt0(xa))&aElementOf0(X15,slsdtgt0(xb)))&sdtpldt0(X14,X15)=xu)))&aElementOf0(xu,xI))&xu!=sz00)&(![X16]:((((![X17]:(![X18]:((~aElementOf0(X17,slsdtgt0(xa))|~aElementOf0(X18,slsdtgt0(xb)))|sdtpldt0(X17,X18)!=X16)))&~aElementOf0(X16,xI))|X16=sz00)|~iLess0(sbrdtbr0(X16),sbrdtbr0(xu))))),inference(variable_rename,[status(thm)],[c76])).
% 65.69/65.93 fof(c79,plain,(![X16]:(![X17]:(![X18]:(((((aElementOf0(skolem0010,slsdtgt0(xa))&aElementOf0(skolem0011,slsdtgt0(xb)))&sdtpldt0(skolem0010,skolem0011)=xu)&aElementOf0(xu,xI))&xu!=sz00)&(((((~aElementOf0(X17,slsdtgt0(xa))|~aElementOf0(X18,slsdtgt0(xb)))|sdtpldt0(X17,X18)!=X16)&~aElementOf0(X16,xI))|X16=sz00)|~iLess0(sbrdtbr0(X16),sbrdtbr0(xu))))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,(((((aElementOf0(skolem0010,slsdtgt0(xa))&aElementOf0(skolem0011,slsdtgt0(xb)))&sdtpldt0(skolem0010,skolem0011)=xu)&aElementOf0(xu,xI))&xu!=sz00)&(![X16]:((((![X17]:(![X18]:((~aElementOf0(X17,slsdtgt0(xa))|~aElementOf0(X18,slsdtgt0(xb)))|sdtpldt0(X17,X18)!=X16)))&~aElementOf0(X16,xI))|X16=sz00)|~iLess0(sbrdtbr0(X16),sbrdtbr0(xu))))),inference(skolemize,[status(esa)],[c77])).])).
% 65.69/65.93 fof(c80,plain,(![X16]:(![X17]:(![X18]:(((((aElementOf0(skolem0010,slsdtgt0(xa))&aElementOf0(skolem0011,slsdtgt0(xb)))&sdtpldt0(skolem0010,skolem0011)=xu)&aElementOf0(xu,xI))&xu!=sz00)&(((((~aElementOf0(X17,slsdtgt0(xa))|~aElementOf0(X18,slsdtgt0(xb)))|sdtpldt0(X17,X18)!=X16)|X16=sz00)|~iLess0(sbrdtbr0(X16),sbrdtbr0(xu)))&((~aElementOf0(X16,xI)|X16=sz00)|~iLess0(sbrdtbr0(X16),sbrdtbr0(xu)))))))),inference(distribute,[status(thm)],[c79])).
% 65.69/65.93 cnf(c87,plain,~aElementOf0(X258,xI)|X258=sz00|~iLess0(sbrdtbr0(X258),sbrdtbr0(xu)),inference(split_conjunct,[status(thm)],[c80])).
% 65.69/65.93 cnf(c861,plain,~aElementOf0(xr,xI)|xr=sz00,inference(resolution,[status(thm)],[c87, c45])).
% 65.69/65.93 cnf(c121037,plain,xr=sz00,inference(resolution,[status(thm)],[c861, c26])).
% 65.69/65.93 cnf(c121094,plain,$false,inference(resolution,[status(thm)],[c121037, c41])).
% 65.69/65.93 % SZS output end CNFRefutation
% 65.69/65.93
% 65.69/65.93 % Initial clauses : 236
% 65.69/65.93 % Processed clauses : 2439
% 65.69/65.93 % Factors computed : 45
% 65.69/65.93 % Resolvents computed: 120696
% 65.69/65.93 % Tautologies deleted: 6
% 65.69/65.93 % Forward subsumed : 268
% 65.69/65.93 % Backward subsumed : 17
% 65.69/65.93 % -------- CPU Time ---------
% 65.69/65.93 % User time : 65.337 s
% 65.69/65.93 % System time : 0.218 s
% 65.69/65.93 % Total time : 65.555 s
%------------------------------------------------------------------------------