%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET960+1 : TPTP v8.1.2. Released v3.2.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:40:25 EDT 2024
% Result : Theorem 148.45s 148.71s
% Output : Refutation 148.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : SET960+1 : TPTP v8.1.2. Released v3.2.0.
% 0.13/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n022.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % 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:45:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 148.45/148.71 % Version: 1.5
% 148.45/148.71 % SZS status Theorem
% 148.45/148.71 % SZS output start CNFRefutation
% 148.45/148.71 cnf(reflexivity,axiom,X35=X35,theory(equality)).
% 148.45/148.71 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_xboole_0)).
% 148.45/148.71 fof(c41,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 148.45/148.71 fof(c42,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c41])).
% 148.45/148.71 fof(c43,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c42])).
% 148.45/148.71 fof(c44,plain,((![X27]:(X27!=empty_set|(![X28]:~in(X28,X27))))&(![X29]:((?[X30]:in(X30,X29))|X29=empty_set))),inference(variable_rename,[status(thm)],[c43])).
% 148.45/148.71 fof(c46,plain,(![X27]:(![X28]:(![X29]:((X27!=empty_set|~in(X28,X27))&(in(skolem0010(X29),X29)|X29=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c45,plain,((![X27]:(X27!=empty_set|(![X28]:~in(X28,X27))))&(![X29]:(in(skolem0010(X29),X29)|X29=empty_set))),inference(skolemize,[status(esa)],[c44])).])).
% 148.45/148.71 cnf(c47,plain,X44!=empty_set|~in(X45,X44),inference(split_conjunct,[status(thm)],[c46])).
% 148.45/148.71 cnf(c48,plain,in(skolem0010(X63),X63)|X63=empty_set,inference(split_conjunct,[status(thm)],[c46])).
% 148.45/148.71 fof(t113_zfmisc_1,conjecture,(![A]:(![B]:(cartesian_product2(A,B)=empty_set<=>(A=empty_set|B=empty_set)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t113_zfmisc_1)).
% 148.45/148.71 fof(c6,negated_conjecture,(~(![A]:(![B]:(cartesian_product2(A,B)=empty_set<=>(A=empty_set|B=empty_set))))),inference(assume_negation,[status(cth)],[t113_zfmisc_1])).
% 148.45/148.71 fof(c7,negated_conjecture,(?[A]:(?[B]:((cartesian_product2(A,B)!=empty_set|(A!=empty_set&B!=empty_set))&(cartesian_product2(A,B)=empty_set|(A=empty_set|B=empty_set))))),inference(fof_nnf,[status(thm)],[c6])).
% 148.45/148.71 fof(c8,negated_conjecture,(?[X2]:(?[X3]:((cartesian_product2(X2,X3)!=empty_set|(X2!=empty_set&X3!=empty_set))&(cartesian_product2(X2,X3)=empty_set|(X2=empty_set|X3=empty_set))))),inference(variable_rename,[status(thm)],[c7])).
% 148.45/148.71 fof(c9,negated_conjecture,((cartesian_product2(skolem0001,skolem0002)!=empty_set|(skolem0001!=empty_set&skolem0002!=empty_set))&(cartesian_product2(skolem0001,skolem0002)=empty_set|(skolem0001=empty_set|skolem0002=empty_set))),inference(skolemize,[status(esa)],[c8])).
% 148.45/148.71 fof(c10,negated_conjecture,(((cartesian_product2(skolem0001,skolem0002)!=empty_set|skolem0001!=empty_set)&(cartesian_product2(skolem0001,skolem0002)!=empty_set|skolem0002!=empty_set))&(cartesian_product2(skolem0001,skolem0002)=empty_set|(skolem0001=empty_set|skolem0002=empty_set))),inference(distribute,[status(thm)],[c9])).
% 148.45/148.71 cnf(c11,negated_conjecture,cartesian_product2(skolem0001,skolem0002)!=empty_set|skolem0001!=empty_set,inference(split_conjunct,[status(thm)],[c10])).
% 148.45/148.71 cnf(c1,axiom,X70!=X69|X68!=X71|cartesian_product2(X70,X68)=cartesian_product2(X69,X71),theory(equality)).
% 148.45/148.71 cnf(c80,plain,X123!=X122|cartesian_product2(X123,X121)=cartesian_product2(X122,X121),inference(resolution,[status(thm)],[c1, reflexivity])).
% 148.45/148.71 cnf(c180,plain,cartesian_product2(X305,X306)=cartesian_product2(empty_set,X306)|in(skolem0010(X305),X305),inference(resolution,[status(thm)],[c80, c48])).
% 148.45/148.71 cnf(transitivity,axiom,X48!=X50|X50!=X49|X48=X49,theory(equality)).
% 148.45/148.71 cnf(symmetry,axiom,X38!=X39|X39=X38,theory(equality)).
% 148.45/148.71 fof(d2_zfmisc_1,axiom,(![A]:(![B]:(![C]:(C=cartesian_product2(A,B)<=>(![D]:(in(D,C)<=>(?[E]:(?[F]:((in(E,A)&in(F,B))&D=ordered_pair(E,F)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_zfmisc_1)).
% 148.45/148.71 fof(c27,plain,(![A]:(![B]:(![C]:((C!=cartesian_product2(A,B)|(![D]:((~in(D,C)|(?[E]:(?[F]:((in(E,A)&in(F,B))&D=ordered_pair(E,F)))))&((![E]:(![F]:((~in(E,A)|~in(F,B))|D!=ordered_pair(E,F))))|in(D,C)))))&((?[D]:((~in(D,C)|(![E]:(![F]:((~in(E,A)|~in(F,B))|D!=ordered_pair(E,F)))))&(in(D,C)|(?[E]:(?[F]:((in(E,A)&in(F,B))&D=ordered_pair(E,F)))))))|C=cartesian_product2(A,B)))))),inference(fof_nnf,[status(thm)],[d2_zfmisc_1])).
% 148.45/148.71 fof(c28,plain,((![A]:(![B]:(![C]:(C!=cartesian_product2(A,B)|((![D]:(~in(D,C)|(?[E]:(?[F]:((in(E,A)&in(F,B))&D=ordered_pair(E,F))))))&(![D]:((![E]:(![F]:((~in(E,A)|~in(F,B))|D!=ordered_pair(E,F))))|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(![E]:(![F]:((~in(E,A)|~in(F,B))|D!=ordered_pair(E,F)))))&(in(D,C)|(?[E]:(?[F]:((in(E,A)&in(F,B))&D=ordered_pair(E,F)))))))|C=cartesian_product2(A,B)))))),inference(shift_quantors,[status(thm)],[c27])).
% 148.45/148.71 fof(c29,plain,((![X10]:(![X11]:(![X12]:(X12!=cartesian_product2(X10,X11)|((![X13]:(~in(X13,X12)|(?[X14]:(?[X15]:((in(X14,X10)&in(X15,X11))&X13=ordered_pair(X14,X15))))))&(![X16]:((![X17]:(![X18]:((~in(X17,X10)|~in(X18,X11))|X16!=ordered_pair(X17,X18))))|in(X16,X12))))))))&(![X19]:(![X20]:(![X21]:((?[X22]:((~in(X22,X21)|(![X23]:(![X24]:((~in(X23,X19)|~in(X24,X20))|X22!=ordered_pair(X23,X24)))))&(in(X22,X21)|(?[X25]:(?[X26]:((in(X25,X19)&in(X26,X20))&X22=ordered_pair(X25,X26)))))))|X21=cartesian_product2(X19,X20)))))),inference(variable_rename,[status(thm)],[c28])).
% 148.45/148.71 fof(c31,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X23]:(![X24]:((X12!=cartesian_product2(X10,X11)|((~in(X13,X12)|((in(skolem0005(X10,X11,X12,X13),X10)&in(skolem0006(X10,X11,X12,X13),X11))&X13=ordered_pair(skolem0005(X10,X11,X12,X13),skolem0006(X10,X11,X12,X13))))&(((~in(X17,X10)|~in(X18,X11))|X16!=ordered_pair(X17,X18))|in(X16,X12))))&(((~in(skolem0007(X19,X20,X21),X21)|((~in(X23,X19)|~in(X24,X20))|skolem0007(X19,X20,X21)!=ordered_pair(X23,X24)))&(in(skolem0007(X19,X20,X21),X21)|((in(skolem0008(X19,X20,X21),X19)&in(skolem0009(X19,X20,X21),X20))&skolem0007(X19,X20,X21)=ordered_pair(skolem0008(X19,X20,X21),skolem0009(X19,X20,X21)))))|X21=cartesian_product2(X19,X20))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X10]:(![X11]:(![X12]:(X12!=cartesian_product2(X10,X11)|((![X13]:(~in(X13,X12)|((in(skolem0005(X10,X11,X12,X13),X10)&in(skolem0006(X10,X11,X12,X13),X11))&X13=ordered_pair(skolem0005(X10,X11,X12,X13),skolem0006(X10,X11,X12,X13)))))&(![X16]:((![X17]:(![X18]:((~in(X17,X10)|~in(X18,X11))|X16!=ordered_pair(X17,X18))))|in(X16,X12))))))))&(![X19]:(![X20]:(![X21]:(((~in(skolem0007(X19,X20,X21),X21)|(![X23]:(![X24]:((~in(X23,X19)|~in(X24,X20))|skolem0007(X19,X20,X21)!=ordered_pair(X23,X24)))))&(in(skolem0007(X19,X20,X21),X21)|((in(skolem0008(X19,X20,X21),X19)&in(skolem0009(X19,X20,X21),X20))&skolem0007(X19,X20,X21)=ordered_pair(skolem0008(X19,X20,X21),skolem0009(X19,X20,X21)))))|X21=cartesian_product2(X19,X20)))))),inference(skolemize,[status(esa)],[c29])).])).
% 148.45/148.71 fof(c32,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X23]:(![X24]:(((((X12!=cartesian_product2(X10,X11)|(~in(X13,X12)|in(skolem0005(X10,X11,X12,X13),X10)))&(X12!=cartesian_product2(X10,X11)|(~in(X13,X12)|in(skolem0006(X10,X11,X12,X13),X11))))&(X12!=cartesian_product2(X10,X11)|(~in(X13,X12)|X13=ordered_pair(skolem0005(X10,X11,X12,X13),skolem0006(X10,X11,X12,X13)))))&(X12!=cartesian_product2(X10,X11)|(((~in(X17,X10)|~in(X18,X11))|X16!=ordered_pair(X17,X18))|in(X16,X12))))&(((~in(skolem0007(X19,X20,X21),X21)|((~in(X23,X19)|~in(X24,X20))|skolem0007(X19,X20,X21)!=ordered_pair(X23,X24)))|X21=cartesian_product2(X19,X20))&((((in(skolem0007(X19,X20,X21),X21)|in(skolem0008(X19,X20,X21),X19))|X21=cartesian_product2(X19,X20))&((in(skolem0007(X19,X20,X21),X21)|in(skolem0009(X19,X20,X21),X20))|X21=cartesian_product2(X19,X20)))&((in(skolem0007(X19,X20,X21),X21)|skolem0007(X19,X20,X21)=ordered_pair(skolem0008(X19,X20,X21),skolem0009(X19,X20,X21)))|X21=cartesian_product2(X19,X20))))))))))))))))),inference(distribute,[status(thm)],[c31])).
% 148.45/148.71 cnf(c38,plain,in(skolem0007(X193,X192,X191),X191)|in(skolem0008(X193,X192,X191),X193)|X191=cartesian_product2(X193,X192),inference(split_conjunct,[status(thm)],[c32])).
% 148.45/148.71 cnf(c324,plain,in(skolem0008(X997,X996,X998),X997)|X998=cartesian_product2(X997,X996)|X998!=empty_set,inference(resolution,[status(thm)],[c38, c47])).
% 148.45/148.71 cnf(c8416,plain,in(skolem0008(X999,X1000,empty_set),X999)|empty_set=cartesian_product2(X999,X1000),inference(resolution,[status(thm)],[c324, reflexivity])).
% 148.45/148.71 cnf(c8448,plain,empty_set=cartesian_product2(X1002,X1001)|X1002!=empty_set,inference(resolution,[status(thm)],[c8416, c47])).
% 148.45/148.71 cnf(c8521,plain,empty_set=cartesian_product2(empty_set,X1003),inference(resolution,[status(thm)],[c8448, reflexivity])).
% 148.45/148.71 cnf(c8773,plain,cartesian_product2(empty_set,X1004)=empty_set,inference(resolution,[status(thm)],[c8521, symmetry])).
% 148.45/148.71 cnf(c8804,plain,X1045!=cartesian_product2(empty_set,X1044)|X1045=empty_set,inference(resolution,[status(thm)],[c8773, transitivity])).
% 148.45/148.71 cnf(c9661,plain,cartesian_product2(X1096,X1097)=empty_set|in(skolem0010(X1096),X1096),inference(resolution,[status(thm)],[c8804, c180])).
% 148.45/148.71 cnf(c10673,plain,in(skolem0010(skolem0001),skolem0001)|skolem0001!=empty_set,inference(resolution,[status(thm)],[c9661, c11])).
% 148.45/148.71 cnf(c10957,plain,in(skolem0010(skolem0001),skolem0001),inference(resolution,[status(thm)],[c10673, c48])).
% 148.45/148.71 cnf(c12,negated_conjecture,cartesian_product2(skolem0001,skolem0002)!=empty_set|skolem0002!=empty_set,inference(split_conjunct,[status(thm)],[c10])).
% 148.45/148.71 cnf(c81,plain,X292!=X291|cartesian_product2(X292,X290)=cartesian_product2(X291,empty_set)|in(skolem0010(X290),X290),inference(resolution,[status(thm)],[c1, c48])).
% 148.45/148.71 cnf(c744,plain,cartesian_product2(X386,X387)=cartesian_product2(X386,empty_set)|in(skolem0010(X387),X387),inference(resolution,[status(thm)],[c81, reflexivity])).
% 148.45/148.71 cnf(c39,plain,in(skolem0007(X205,X204,X203),X203)|in(skolem0009(X205,X204,X203),X204)|X203=cartesian_product2(X205,X204),inference(split_conjunct,[status(thm)],[c32])).
% 148.45/148.71 cnf(c384,plain,in(skolem0009(X2537,X2536,X2538),X2536)|X2538=cartesian_product2(X2537,X2536)|X2538!=empty_set,inference(resolution,[status(thm)],[c39, c47])).
% 148.45/148.71 cnf(c32958,plain,in(skolem0009(X2561,X2562,empty_set),X2562)|empty_set=cartesian_product2(X2561,X2562),inference(resolution,[status(thm)],[c384, reflexivity])).
% 148.45/148.71 cnf(c33169,plain,empty_set=cartesian_product2(X2563,X2564)|X2564!=empty_set,inference(resolution,[status(thm)],[c32958, c47])).
% 148.45/148.71 cnf(c33297,plain,empty_set=cartesian_product2(X2565,empty_set),inference(resolution,[status(thm)],[c33169, reflexivity])).
% 148.45/148.71 cnf(c33404,plain,cartesian_product2(X2571,empty_set)=empty_set,inference(resolution,[status(thm)],[c33297, symmetry])).
% 148.45/148.71 cnf(c33608,plain,X2715!=cartesian_product2(X2714,empty_set)|X2715=empty_set,inference(resolution,[status(thm)],[c33404, transitivity])).
% 148.45/148.71 cnf(c37111,plain,cartesian_product2(X2881,X2880)=empty_set|in(skolem0010(X2880),X2880),inference(resolution,[status(thm)],[c33608, c744])).
% 148.45/148.71 cnf(c39670,plain,in(skolem0010(skolem0002),skolem0002)|skolem0002!=empty_set,inference(resolution,[status(thm)],[c37111, c12])).
% 148.45/148.71 cnf(c40070,plain,in(skolem0010(skolem0002),skolem0002),inference(resolution,[status(thm)],[c39670, c48])).
% 148.45/148.71 cnf(c36,plain,X165!=cartesian_product2(X169,X167)|~in(X166,X169)|~in(X170,X167)|X168!=ordered_pair(X166,X170)|in(X168,X165),inference(split_conjunct,[status(thm)],[c32])).
% 148.45/148.71 cnf(c302,plain,X1641!=cartesian_product2(X1639,X1640)|~in(X1643,X1639)|~in(X1642,X1640)|in(ordered_pair(X1643,X1642),X1641),inference(resolution,[status(thm)],[c36, reflexivity])).
% 148.45/148.71 cnf(c13,negated_conjecture,cartesian_product2(skolem0001,skolem0002)=empty_set|skolem0001=empty_set|skolem0002=empty_set,inference(split_conjunct,[status(thm)],[c10])).
% 148.45/148.71 cnf(c129,plain,skolem0001=empty_set|skolem0002=empty_set|empty_set=cartesian_product2(skolem0001,skolem0002),inference(resolution,[status(thm)],[c13, symmetry])).
% 148.45/148.71 cnf(c11225,plain,skolem0001!=empty_set,inference(resolution,[status(thm)],[c10957, c47])).
% 148.45/148.71 cnf(c11239,plain,skolem0002=empty_set|empty_set=cartesian_product2(skolem0001,skolem0002),inference(resolution,[status(thm)],[c11225, c129])).
% 148.45/148.71 cnf(c40085,plain,skolem0002!=empty_set,inference(resolution,[status(thm)],[c40070, c47])).
% 148.45/148.71 cnf(c40108,plain,empty_set=cartesian_product2(skolem0001,skolem0002),inference(resolution,[status(thm)],[c40085, c11239])).
% 148.45/148.71 cnf(c40424,plain,~in(X9111,skolem0001)|~in(X9112,skolem0002)|in(ordered_pair(X9111,X9112),empty_set),inference(resolution,[status(thm)],[c40108, c302])).
% 148.45/148.71 cnf(c156178,plain,~in(X9113,skolem0001)|in(ordered_pair(X9113,skolem0010(skolem0002)),empty_set),inference(resolution,[status(thm)],[c40424, c40070])).
% 148.45/148.71 cnf(c156700,plain,in(ordered_pair(skolem0010(skolem0001),skolem0010(skolem0002)),empty_set),inference(resolution,[status(thm)],[c156178, c10957])).
% 148.45/148.71 cnf(c156749,plain,empty_set!=empty_set,inference(resolution,[status(thm)],[c156700, c47])).
% 148.45/148.71 cnf(c156959,plain,$false,inference(resolution,[status(thm)],[c156749, reflexivity])).
% 148.45/148.71 % SZS output end CNFRefutation
% 148.45/148.71
% 148.45/148.71 % Initial clauses : 29
% 148.45/148.71 % Processed clauses : 1630
% 148.45/148.71 % Factors computed : 60
% 148.45/148.71 % Resolvents computed: 156850
% 148.45/148.71 % Tautologies deleted: 14
% 148.45/148.71 % Forward subsumed : 2995
% 148.45/148.71 % Backward subsumed : 163
% 148.45/148.71 % -------- CPU Time ---------
% 148.45/148.71 % User time : 147.891 s
% 148.45/148.71 % System time : 0.379 s
% 148.45/148.71 % Total time : 148.270 s
%------------------------------------------------------------------------------