%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET977+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:40:26 EDT 2024
% Result : Theorem 3.38s 3.52s
% Output : Refutation 3.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET977+1 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 18:28:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 3.38/3.52 % Version: 1.5
% 3.38/3.52 % SZS status Theorem
% 3.38/3.52 % SZS output start CNFRefutation
% 3.38/3.52 fof(t130_zfmisc_1,conjecture,(![A]:(![B]:(A!=empty_set=>(cartesian_product2(singleton(B),A)!=empty_set&cartesian_product2(A,singleton(B))!=empty_set)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t130_zfmisc_1)).
% 3.38/3.52 fof(c6,negated_conjecture,(~(![A]:(![B]:(A!=empty_set=>(cartesian_product2(singleton(B),A)!=empty_set&cartesian_product2(A,singleton(B))!=empty_set))))),inference(assume_negation,[status(cth)],[t130_zfmisc_1])).
% 3.38/3.52 fof(c7,negated_conjecture,(?[A]:(?[B]:(A!=empty_set&(cartesian_product2(singleton(B),A)=empty_set|cartesian_product2(A,singleton(B))=empty_set)))),inference(fof_nnf,[status(thm)],[c6])).
% 3.38/3.52 fof(c8,negated_conjecture,(?[A]:(A!=empty_set&((?[B]:cartesian_product2(singleton(B),A)=empty_set)|(?[B]:cartesian_product2(A,singleton(B))=empty_set)))),inference(shift_quantors,[status(thm)],[c7])).
% 3.38/3.52 fof(c9,negated_conjecture,(?[X2]:(X2!=empty_set&((?[X3]:cartesian_product2(singleton(X3),X2)=empty_set)|(?[X4]:cartesian_product2(X2,singleton(X4))=empty_set)))),inference(variable_rename,[status(thm)],[c8])).
% 3.38/3.52 fof(c10,negated_conjecture,(skolem0001!=empty_set&(cartesian_product2(singleton(skolem0002),skolem0001)=empty_set|cartesian_product2(skolem0001,singleton(skolem0003))=empty_set)),inference(skolemize,[status(esa)],[c9])).
% 3.38/3.52 cnf(c12,negated_conjecture,cartesian_product2(singleton(skolem0002),skolem0001)=empty_set|cartesian_product2(skolem0001,singleton(skolem0003))=empty_set,inference(split_conjunct,[status(thm)],[c10])).
% 3.38/3.52 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_xboole_0)).
% 3.38/3.52 fof(c42,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 3.38/3.52 fof(c43,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c42])).
% 3.38/3.52 fof(c44,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c43])).
% 3.38/3.52 fof(c45,plain,((![X27]:(X27!=empty_set|(![X28]:~in(X28,X27))))&(![X29]:((?[X30]:in(X30,X29))|X29=empty_set))),inference(variable_rename,[status(thm)],[c44])).
% 3.38/3.52 fof(c47,plain,(![X27]:(![X28]:(![X29]:((X27!=empty_set|~in(X28,X27))&(in(skolem0006(X29),X29)|X29=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X27]:(X27!=empty_set|(![X28]:~in(X28,X27))))&(![X29]:(in(skolem0006(X29),X29)|X29=empty_set))),inference(skolemize,[status(esa)],[c45])).])).
% 3.38/3.52 cnf(c48,plain,X45!=empty_set|~in(X44,X45),inference(split_conjunct,[status(thm)],[c47])).
% 3.38/3.52 cnf(c11,negated_conjecture,skolem0001!=empty_set,inference(split_conjunct,[status(thm)],[c10])).
% 3.38/3.52 cnf(c49,plain,in(skolem0006(X63),X63)|X63=empty_set,inference(split_conjunct,[status(thm)],[c47])).
% 3.38/3.52 cnf(c69,plain,in(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c49, c11])).
% 3.38/3.52 cnf(reflexivity,axiom,X35=X35,theory(equality)).
% 3.38/3.52 fof(t129_zfmisc_1,axiom,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))<=>(in(A,C)&B=D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t129_zfmisc_1)).
% 3.38/3.52 fof(c13,plain,(![A]:(![B]:(![C]:(![D]:((~in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))|(in(A,C)&B=D))&((~in(A,C)|B!=D)|in(ordered_pair(A,B),cartesian_product2(C,singleton(D))))))))),inference(fof_nnf,[status(thm)],[t129_zfmisc_1])).
% 3.38/3.52 fof(c14,plain,((![A]:(![B]:(![C]:(![D]:(~in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))|(in(A,C)&B=D))))))&(![A]:(![B]:(![C]:(![D]:((~in(A,C)|B!=D)|in(ordered_pair(A,B),cartesian_product2(C,singleton(D))))))))),inference(shift_quantors,[status(thm)],[c13])).
% 3.38/3.52 fof(c16,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~in(ordered_pair(X5,X6),cartesian_product2(X7,singleton(X8)))|(in(X5,X7)&X6=X8))&((~in(X9,X11)|X10!=X12)|in(ordered_pair(X9,X10),cartesian_product2(X11,singleton(X12))))))))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X5]:(![X6]:(![X7]:(![X8]:(~in(ordered_pair(X5,X6),cartesian_product2(X7,singleton(X8)))|(in(X5,X7)&X6=X8))))))&(![X9]:(![X10]:(![X11]:(![X12]:((~in(X9,X11)|X10!=X12)|in(ordered_pair(X9,X10),cartesian_product2(X11,singleton(X12))))))))),inference(variable_rename,[status(thm)],[c14])).])).
% 3.38/3.52 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((~in(ordered_pair(X5,X6),cartesian_product2(X7,singleton(X8)))|in(X5,X7))&(~in(ordered_pair(X5,X6),cartesian_product2(X7,singleton(X8)))|X6=X8))&((~in(X9,X11)|X10!=X12)|in(ordered_pair(X9,X10),cartesian_product2(X11,singleton(X12))))))))))))),inference(distribute,[status(thm)],[c16])).
% 3.38/3.52 cnf(c20,plain,~in(X134,X132)|X133!=X135|in(ordered_pair(X134,X133),cartesian_product2(X132,singleton(X135))),inference(split_conjunct,[status(thm)],[c17])).
% 3.38/3.52 cnf(c163,plain,~in(X218,X216)|in(ordered_pair(X218,X217),cartesian_product2(X216,singleton(X217))),inference(resolution,[status(thm)],[c20, reflexivity])).
% 3.38/3.52 cnf(c420,plain,in(ordered_pair(skolem0006(skolem0001),X263),cartesian_product2(skolem0001,singleton(X263))),inference(resolution,[status(thm)],[c163, c69])).
% 3.38/3.52 cnf(c637,plain,cartesian_product2(skolem0001,singleton(X265))!=empty_set,inference(resolution,[status(thm)],[c420, c48])).
% 3.38/3.52 cnf(c644,plain,cartesian_product2(singleton(skolem0002),skolem0001)=empty_set,inference(resolution,[status(thm)],[c637, c12])).
% 3.38/3.52 fof(t128_zfmisc_1,axiom,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(singleton(C),D))<=>(A=C&in(B,D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t128_zfmisc_1)).
% 3.38/3.52 fof(c21,plain,(![A]:(![B]:(![C]:(![D]:((~in(ordered_pair(A,B),cartesian_product2(singleton(C),D))|(A=C&in(B,D)))&((A!=C|~in(B,D))|in(ordered_pair(A,B),cartesian_product2(singleton(C),D)))))))),inference(fof_nnf,[status(thm)],[t128_zfmisc_1])).
% 3.38/3.52 fof(c22,plain,((![A]:(![B]:(![C]:(![D]:(~in(ordered_pair(A,B),cartesian_product2(singleton(C),D))|(A=C&in(B,D)))))))&(![A]:(![B]:(![C]:(![D]:((A!=C|~in(B,D))|in(ordered_pair(A,B),cartesian_product2(singleton(C),D)))))))),inference(shift_quantors,[status(thm)],[c21])).
% 3.38/3.52 fof(c24,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((~in(ordered_pair(X13,X14),cartesian_product2(singleton(X15),X16))|(X13=X15&in(X14,X16)))&((X17!=X19|~in(X18,X20))|in(ordered_pair(X17,X18),cartesian_product2(singleton(X19),X20)))))))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X13]:(![X14]:(![X15]:(![X16]:(~in(ordered_pair(X13,X14),cartesian_product2(singleton(X15),X16))|(X13=X15&in(X14,X16)))))))&(![X17]:(![X18]:(![X19]:(![X20]:((X17!=X19|~in(X18,X20))|in(ordered_pair(X17,X18),cartesian_product2(singleton(X19),X20)))))))),inference(variable_rename,[status(thm)],[c22])).])).
% 3.38/3.52 fof(c25,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(((~in(ordered_pair(X13,X14),cartesian_product2(singleton(X15),X16))|X13=X15)&(~in(ordered_pair(X13,X14),cartesian_product2(singleton(X15),X16))|in(X14,X16)))&((X17!=X19|~in(X18,X20))|in(ordered_pair(X17,X18),cartesian_product2(singleton(X19),X20)))))))))))),inference(distribute,[status(thm)],[c24])).
% 3.38/3.52 cnf(c28,plain,X169!=X171|~in(X170,X168)|in(ordered_pair(X169,X170),cartesian_product2(singleton(X171),X168)),inference(split_conjunct,[status(thm)],[c25])).
% 3.38/3.52 cnf(c262,plain,X1271!=X1272|in(ordered_pair(X1271,skolem0006(skolem0001)),cartesian_product2(singleton(X1272),skolem0001)),inference(resolution,[status(thm)],[c28, c69])).
% 3.38/3.52 cnf(c10294,plain,in(ordered_pair(X1273,skolem0006(skolem0001)),cartesian_product2(singleton(X1273),skolem0001)),inference(resolution,[status(thm)],[c262, reflexivity])).
% 3.38/3.52 cnf(c10344,plain,cartesian_product2(singleton(X1275),skolem0001)!=empty_set,inference(resolution,[status(thm)],[c10294, c48])).
% 3.38/3.52 cnf(c10352,plain,$false,inference(resolution,[status(thm)],[c10344, c644])).
% 3.38/3.52 % SZS output end CNFRefutation
% 3.38/3.52
% 3.38/3.52 % Initial clauses : 26
% 3.38/3.52 % Processed clauses : 401
% 3.38/3.52 % Factors computed : 7
% 3.38/3.52 % Resolvents computed: 10292
% 3.38/3.52 % Tautologies deleted: 4
% 3.38/3.52 % Forward subsumed : 373
% 3.38/3.52 % Backward subsumed : 18
% 3.38/3.52 % -------- CPU Time ---------
% 3.38/3.52 % User time : 3.116 s
% 3.38/3.52 % System time : 0.032 s
% 3.38/3.52 % Total time : 3.148 s
%------------------------------------------------------------------------------