%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU280+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:41:00 EDT 2024
% Result : Theorem 16.11s 16.29s
% Output : Refutation 16.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU280+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 11:44:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 16.11/16.29 % Version: 1.5
% 16.11/16.29 % SZS status Theorem
% 16.11/16.29 % SZS output start CNFRefutation
% 16.11/16.29 fof(s1_xboole_0__e6_22__wellord2,conjecture,(![A]:(?[B]:(![C]:(in(C,B)<=>(in(C,A)&ordinal(C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_xboole_0__e6_22__wellord2)).
% 16.11/16.29 fof(c47,negated_conjecture,(~(![A]:(?[B]:(![C]:(in(C,B)<=>(in(C,A)&ordinal(C))))))),inference(assume_negation,[status(cth)],[s1_xboole_0__e6_22__wellord2])).
% 16.11/16.29 fof(c48,negated_conjecture,(?[A]:(![B]:(?[C]:((~in(C,B)|(~in(C,A)|~ordinal(C)))&(in(C,B)|(in(C,A)&ordinal(C))))))),inference(fof_nnf,[status(thm)],[c47])).
% 16.11/16.29 fof(c49,negated_conjecture,(?[X16]:(![X17]:(?[X18]:((~in(X18,X17)|(~in(X18,X16)|~ordinal(X18)))&(in(X18,X17)|(in(X18,X16)&ordinal(X18))))))),inference(variable_rename,[status(thm)],[c48])).
% 16.11/16.29 fof(c50,negated_conjecture,(![X17]:((~in(skolem0008(X17),X17)|(~in(skolem0008(X17),skolem0007)|~ordinal(skolem0008(X17))))&(in(skolem0008(X17),X17)|(in(skolem0008(X17),skolem0007)&ordinal(skolem0008(X17)))))),inference(skolemize,[status(esa)],[c49])).
% 16.11/16.29 fof(c51,negated_conjecture,(![X17]:((~in(skolem0008(X17),X17)|(~in(skolem0008(X17),skolem0007)|~ordinal(skolem0008(X17))))&((in(skolem0008(X17),X17)|in(skolem0008(X17),skolem0007))&(in(skolem0008(X17),X17)|ordinal(skolem0008(X17)))))),inference(distribute,[status(thm)],[c50])).
% 16.11/16.29 cnf(c54,negated_conjecture,in(skolem0008(X50),X50)|ordinal(skolem0008(X50)),inference(split_conjunct,[status(thm)],[c51])).
% 16.11/16.29 fof(s1_tarski__e6_22__wellord2__1,axiom,(![A]:((![B]:(![C]:(![D]:((((B=C&ordinal(C))&B=D)&ordinal(D))=>C=D))))=>(?[B]:(![C]:(in(C,B)<=>(?[D]:((in(D,A)&D=C)&ordinal(C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', s1_tarski__e6_22__wellord2__1)).
% 16.11/16.29 fof(c4,plain,(![A]:((?[B]:(?[C]:(?[D]:((((B=C&ordinal(C))&B=D)&ordinal(D))&C!=D))))|(?[B]:(![C]:((~in(C,B)|(?[D]:((in(D,A)&D=C)&ordinal(C))))&((![D]:((~in(D,A)|D!=C)|~ordinal(C)))|in(C,B))))))),inference(fof_nnf,[status(thm)],[s1_tarski__e6_22__wellord2__1])).
% 16.11/16.29 fof(c5,plain,((?[B]:(?[C]:(?[D]:((((B=C&ordinal(C))&B=D)&ordinal(D))&C!=D))))|(![A]:(?[B]:((![C]:(~in(C,B)|((?[D]:(in(D,A)&D=C))&ordinal(C))))&(![C]:(((![D]:(~in(D,A)|D!=C))|~ordinal(C))|in(C,B))))))),inference(shift_quantors,[status(thm)],[c4])).
% 16.11/16.29 fof(c6,plain,((?[X2]:(?[X3]:(?[X4]:((((X2=X3&ordinal(X3))&X2=X4)&ordinal(X4))&X3!=X4))))|(![X5]:(?[X6]:((![X7]:(~in(X7,X6)|((?[X8]:(in(X8,X5)&X8=X7))&ordinal(X7))))&(![X9]:(((![X10]:(~in(X10,X5)|X10!=X9))|~ordinal(X9))|in(X9,X6))))))),inference(variable_rename,[status(thm)],[c5])).
% 16.11/16.29 fof(c8,plain,(![X5]:(![X7]:(![X9]:(![X10]:(((((skolem0001=skolem0002&ordinal(skolem0002))&skolem0001=skolem0003)&ordinal(skolem0003))&skolem0002!=skolem0003)|((~in(X7,skolem0004(X5))|((in(skolem0005(X5,X7),X5)&skolem0005(X5,X7)=X7)&ordinal(X7)))&(((~in(X10,X5)|X10!=X9)|~ordinal(X9))|in(X9,skolem0004(X5))))))))),inference(shift_quantors,[status(thm)],[fof(c7,plain,(((((skolem0001=skolem0002&ordinal(skolem0002))&skolem0001=skolem0003)&ordinal(skolem0003))&skolem0002!=skolem0003)|(![X5]:((![X7]:(~in(X7,skolem0004(X5))|((in(skolem0005(X5,X7),X5)&skolem0005(X5,X7)=X7)&ordinal(X7))))&(![X9]:(((![X10]:(~in(X10,X5)|X10!=X9))|~ordinal(X9))|in(X9,skolem0004(X5))))))),inference(skolemize,[status(esa)],[c6])).])).
% 16.11/16.29 fof(c9,plain,(![X5]:(![X7]:(![X9]:(![X10]:((((((((skolem0001=skolem0002|(~in(X7,skolem0004(X5))|in(skolem0005(X5,X7),X5)))&(skolem0001=skolem0002|(~in(X7,skolem0004(X5))|skolem0005(X5,X7)=X7)))&(skolem0001=skolem0002|(~in(X7,skolem0004(X5))|ordinal(X7))))&(skolem0001=skolem0002|(((~in(X10,X5)|X10!=X9)|~ordinal(X9))|in(X9,skolem0004(X5)))))&((((ordinal(skolem0002)|(~in(X7,skolem0004(X5))|in(skolem0005(X5,X7),X5)))&(ordinal(skolem0002)|(~in(X7,skolem0004(X5))|skolem0005(X5,X7)=X7)))&(ordinal(skolem0002)|(~in(X7,skolem0004(X5))|ordinal(X7))))&(ordinal(skolem0002)|(((~in(X10,X5)|X10!=X9)|~ordinal(X9))|in(X9,skolem0004(X5))))))&((((skolem0001=skolem0003|(~in(X7,skolem0004(X5))|in(skolem0005(X5,X7),X5)))&(skolem0001=skolem0003|(~in(X7,skolem0004(X5))|skolem0005(X5,X7)=X7)))&(skolem0001=skolem0003|(~in(X7,skolem0004(X5))|ordinal(X7))))&(skolem0001=skolem0003|(((~in(X10,X5)|X10!=X9)|~ordinal(X9))|in(X9,skolem0004(X5))))))&((((ordinal(skolem0003)|(~in(X7,skolem0004(X5))|in(skolem0005(X5,X7),X5)))&(ordinal(skolem0003)|(~in(X7,skolem0004(X5))|skolem0005(X5,X7)=X7)))&(ordinal(skolem0003)|(~in(X7,skolem0004(X5))|ordinal(X7))))&(ordinal(skolem0003)|(((~in(X10,X5)|X10!=X9)|~ordinal(X9))|in(X9,skolem0004(X5))))))&((((skolem0002!=skolem0003|(~in(X7,skolem0004(X5))|in(skolem0005(X5,X7),X5)))&(skolem0002!=skolem0003|(~in(X7,skolem0004(X5))|skolem0005(X5,X7)=X7)))&(skolem0002!=skolem0003|(~in(X7,skolem0004(X5))|ordinal(X7))))&(skolem0002!=skolem0003|(((~in(X10,X5)|X10!=X9)|~ordinal(X9))|in(X9,skolem0004(X5)))))))))),inference(distribute,[status(thm)],[c8])).
% 16.11/16.29 cnf(c28,plain,skolem0002!=skolem0003|~in(X139,skolem0004(X138))|ordinal(X139),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c277,plain,skolem0002!=skolem0003|ordinal(skolem0008(skolem0004(X140))),inference(resolution,[status(thm)],[c28, c54])).
% 16.11/16.29 cnf(symmetry,axiom,X22!=X21|X21=X22,theory(equality)).
% 16.11/16.29 cnf(c20,plain,skolem0001=skolem0003|~in(X113,skolem0004(X112))|ordinal(X113),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c197,plain,skolem0001=skolem0003|ordinal(skolem0008(skolem0004(X122))),inference(resolution,[status(thm)],[c20, c54])).
% 16.11/16.29 cnf(c218,plain,ordinal(skolem0008(skolem0004(X124)))|skolem0003=skolem0001,inference(resolution,[status(thm)],[c197, symmetry])).
% 16.11/16.29 cnf(transitivity,axiom,X29!=X28|X28!=X27|X29=X27,theory(equality)).
% 16.11/16.29 cnf(c12,plain,skolem0001=skolem0002|~in(X63,skolem0004(X62))|ordinal(X63),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c90,plain,skolem0001=skolem0002|ordinal(skolem0008(skolem0004(X103))),inference(resolution,[status(thm)],[c12, c54])).
% 16.11/16.29 cnf(c152,plain,ordinal(skolem0008(skolem0004(X223)))|X222!=skolem0001|X222=skolem0002,inference(resolution,[status(thm)],[c90, transitivity])).
% 16.11/16.29 cnf(c434,plain,ordinal(skolem0008(skolem0004(X527)))|skolem0003=skolem0002|ordinal(skolem0008(skolem0004(X528))),inference(resolution,[status(thm)],[c152, c218])).
% 16.11/16.29 cnf(c831,plain,ordinal(skolem0008(skolem0004(X529)))|skolem0003=skolem0002,inference(factor,[status(thm)],[c434])).
% 16.11/16.29 cnf(c869,plain,ordinal(skolem0008(skolem0004(X534)))|skolem0002=skolem0003,inference(resolution,[status(thm)],[c831, symmetry])).
% 16.11/16.29 cnf(c920,plain,ordinal(skolem0008(skolem0004(X546)))|ordinal(skolem0008(skolem0004(X547))),inference(resolution,[status(thm)],[c869, c277])).
% 16.11/16.29 cnf(c964,plain,ordinal(skolem0008(skolem0004(X548))),inference(factor,[status(thm)],[c920])).
% 16.11/16.29 cnf(c53,negated_conjecture,in(skolem0008(X102),X102)|in(skolem0008(X102),skolem0007),inference(split_conjunct,[status(thm)],[c51])).
% 16.11/16.29 cnf(reflexivity,axiom,X19=X19,theory(equality)).
% 16.11/16.29 cnf(c29,plain,skolem0002!=skolem0003|~in(X164,X166)|X164!=X165|~ordinal(X165)|in(X165,skolem0004(X166)),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c313,plain,skolem0002!=skolem0003|~in(X513,X512)|~ordinal(X513)|in(X513,skolem0004(X512)),inference(resolution,[status(thm)],[c29, reflexivity])).
% 16.11/16.29 cnf(c785,plain,skolem0002!=skolem0003|~ordinal(skolem0008(X1717))|in(skolem0008(X1717),skolem0004(skolem0007))|in(skolem0008(X1717),X1717),inference(resolution,[status(thm)],[c313, c53])).
% 16.11/16.29 cnf(c7924,plain,skolem0002!=skolem0003|in(skolem0008(X1719),skolem0004(skolem0007))|in(skolem0008(X1719),X1719),inference(resolution,[status(thm)],[c785, c54])).
% 16.11/16.29 cnf(c13,plain,skolem0001=skolem0002|~in(X69,X71)|X69!=X70|~ordinal(X70)|in(X70,skolem0004(X71)),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c103,plain,skolem0001=skolem0002|~in(X278,X277)|~ordinal(X278)|in(X278,skolem0004(X277)),inference(resolution,[status(thm)],[c13, reflexivity])).
% 16.11/16.29 cnf(c512,plain,skolem0001=skolem0002|~ordinal(skolem0008(X1061))|in(skolem0008(X1061),skolem0004(skolem0007))|in(skolem0008(X1061),X1061),inference(resolution,[status(thm)],[c103, c53])).
% 16.11/16.29 cnf(c2096,plain,skolem0001=skolem0002|in(skolem0008(X1062),skolem0004(skolem0007))|in(skolem0008(X1062),X1062),inference(resolution,[status(thm)],[c512, c54])).
% 16.11/16.29 cnf(c2098,plain,skolem0001=skolem0002|in(skolem0008(skolem0004(skolem0007)),skolem0004(skolem0007)),inference(factor,[status(thm)],[c2096])).
% 16.11/16.29 cnf(c52,negated_conjecture,~in(skolem0008(X172),X172)|~in(skolem0008(X172),skolem0007)|~ordinal(skolem0008(X172)),inference(split_conjunct,[status(thm)],[c51])).
% 16.11/16.29 cnf(c11,plain,skolem0001=skolem0002|~in(X55,skolem0004(X54))|skolem0005(X54,X55)=X55,inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c145,plain,in(skolem0008(skolem0004(X447)),skolem0007)|skolem0001=skolem0002|skolem0005(X447,skolem0008(skolem0004(X447)))=skolem0008(skolem0004(X447)),inference(resolution,[status(thm)],[c53, c11])).
% 16.11/16.29 cnf(c0,axiom,X36!=X37|X35!=X38|~in(X36,X35)|in(X37,X38),theory(equality)).
% 16.11/16.29 cnf(c10,plain,skolem0001=skolem0002|~in(X48,skolem0004(X47))|in(skolem0005(X47,X48),X47),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c138,plain,in(skolem0008(skolem0004(X381)),skolem0007)|skolem0001=skolem0002|in(skolem0005(X381,skolem0008(skolem0004(X381))),X381),inference(resolution,[status(thm)],[c53, c10])).
% 16.11/16.29 cnf(c606,plain,in(skolem0008(skolem0004(X1200)),skolem0007)|skolem0001=skolem0002|skolem0005(X1200,skolem0008(skolem0004(X1200)))!=X1202|X1200!=X1201|in(X1202,X1201),inference(resolution,[status(thm)],[c138, c0])).
% 16.11/16.29 cnf(c3513,plain,in(skolem0008(skolem0004(X2648)),skolem0007)|skolem0001=skolem0002|X2648!=X2647|in(skolem0008(skolem0004(X2648)),X2647),inference(resolution,[status(thm)],[c606, c145])).
% 16.11/16.29 cnf(c13635,plain,in(skolem0008(skolem0004(X2649)),skolem0007)|skolem0001=skolem0002|in(skolem0008(skolem0004(X2649)),X2649),inference(resolution,[status(thm)],[c3513, reflexivity])).
% 16.11/16.29 cnf(c13693,plain,in(skolem0008(skolem0004(skolem0007)),skolem0007)|skolem0001=skolem0002,inference(factor,[status(thm)],[c13635])).
% 16.11/16.29 cnf(c13748,plain,skolem0001=skolem0002|~in(skolem0008(skolem0004(skolem0007)),skolem0004(skolem0007))|~ordinal(skolem0008(skolem0004(skolem0007))),inference(resolution,[status(thm)],[c13693, c52])).
% 16.11/16.29 cnf(c14070,plain,skolem0001=skolem0002|~ordinal(skolem0008(skolem0004(skolem0007))),inference(resolution,[status(thm)],[c13748, c2098])).
% 16.11/16.29 cnf(c14124,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c14070, c964])).
% 16.11/16.29 cnf(c14134,plain,X2691!=skolem0001|X2691=skolem0002,inference(resolution,[status(thm)],[c14124, transitivity])).
% 16.11/16.29 cnf(c21,plain,skolem0001=skolem0003|~in(X119,X121)|X119!=X120|~ordinal(X120)|in(X120,skolem0004(X121)),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c208,plain,skolem0001=skolem0003|~in(X511,X510)|~ordinal(X511)|in(X511,skolem0004(X510)),inference(resolution,[status(thm)],[c21, reflexivity])).
% 16.11/16.29 cnf(c771,plain,skolem0001=skolem0003|~ordinal(skolem0008(X1607))|in(skolem0008(X1607),skolem0004(skolem0007))|in(skolem0008(X1607),X1607),inference(resolution,[status(thm)],[c208, c53])).
% 16.11/16.29 cnf(c6593,plain,skolem0001=skolem0003|in(skolem0008(X1608),skolem0004(skolem0007))|in(skolem0008(X1608),X1608),inference(resolution,[status(thm)],[c771, c54])).
% 16.11/16.29 cnf(c6594,plain,skolem0001=skolem0003|in(skolem0008(skolem0004(skolem0007)),skolem0004(skolem0007)),inference(factor,[status(thm)],[c6593])).
% 16.11/16.29 cnf(c19,plain,skolem0001=skolem0003|~in(X106,skolem0004(X105))|skolem0005(X105,X106)=X106,inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c163,plain,skolem0001=skolem0003|skolem0005(X524,skolem0008(skolem0004(X524)))=skolem0008(skolem0004(X524))|in(skolem0008(skolem0004(X524)),skolem0007),inference(resolution,[status(thm)],[c19, c53])).
% 16.11/16.29 cnf(c18,plain,skolem0001=skolem0003|~in(X101,skolem0004(X100))|in(skolem0005(X100,X101),X100),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c139,plain,in(skolem0008(skolem0004(X392)),skolem0007)|skolem0001=skolem0003|in(skolem0005(X392,skolem0008(skolem0004(X392))),X392),inference(resolution,[status(thm)],[c53, c18])).
% 16.11/16.29 cnf(c648,plain,in(skolem0008(skolem0004(X1369)),skolem0007)|skolem0001=skolem0003|skolem0005(X1369,skolem0008(skolem0004(X1369)))!=X1371|X1369!=X1370|in(X1371,X1370),inference(resolution,[status(thm)],[c139, c0])).
% 16.11/16.29 cnf(c4780,plain,in(skolem0008(skolem0004(X3033)),skolem0007)|skolem0001=skolem0003|X3033!=X3032|in(skolem0008(skolem0004(X3033)),X3032),inference(resolution,[status(thm)],[c648, c163])).
% 16.11/16.29 cnf(c15798,plain,in(skolem0008(skolem0004(X3034)),skolem0007)|skolem0001=skolem0003|in(skolem0008(skolem0004(X3034)),X3034),inference(resolution,[status(thm)],[c4780, reflexivity])).
% 16.11/16.29 cnf(c15839,plain,in(skolem0008(skolem0004(skolem0007)),skolem0007)|skolem0001=skolem0003,inference(factor,[status(thm)],[c15798])).
% 16.11/16.29 cnf(c15894,plain,skolem0001=skolem0003|~in(skolem0008(skolem0004(skolem0007)),skolem0004(skolem0007))|~ordinal(skolem0008(skolem0004(skolem0007))),inference(resolution,[status(thm)],[c15839, c52])).
% 16.11/16.29 cnf(c16634,plain,skolem0001=skolem0003|~ordinal(skolem0008(skolem0004(skolem0007))),inference(resolution,[status(thm)],[c15894, c6594])).
% 16.11/16.29 cnf(c16665,plain,skolem0001=skolem0003,inference(resolution,[status(thm)],[c16634, c964])).
% 16.11/16.29 cnf(c16674,plain,skolem0003=skolem0001,inference(resolution,[status(thm)],[c16665, symmetry])).
% 16.11/16.29 cnf(c16705,plain,skolem0003=skolem0002,inference(resolution,[status(thm)],[c16674, c14134])).
% 16.11/16.29 cnf(c16733,plain,skolem0002=skolem0003,inference(resolution,[status(thm)],[c16705, symmetry])).
% 16.11/16.29 cnf(c16783,plain,in(skolem0008(X3136),skolem0004(skolem0007))|in(skolem0008(X3136),X3136),inference(resolution,[status(thm)],[c16733, c7924])).
% 16.11/16.29 cnf(c16852,plain,in(skolem0008(skolem0004(skolem0007)),skolem0004(skolem0007)),inference(factor,[status(thm)],[c16783])).
% 16.11/16.29 cnf(c26,plain,skolem0002!=skolem0003|~in(X151,skolem0004(X150))|in(skolem0005(X150,X151),X150),inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c16873,plain,skolem0002!=skolem0003|in(skolem0005(skolem0007,skolem0008(skolem0004(skolem0007))),skolem0007),inference(resolution,[status(thm)],[c16852, c26])).
% 16.11/16.29 cnf(c16914,plain,in(skolem0005(skolem0007,skolem0008(skolem0004(skolem0007))),skolem0007),inference(resolution,[status(thm)],[c16873, c16733])).
% 16.11/16.29 cnf(c16917,plain,skolem0005(skolem0007,skolem0008(skolem0004(skolem0007)))!=X3256|skolem0007!=X3255|in(X3256,X3255),inference(resolution,[status(thm)],[c16914, c0])).
% 16.11/16.29 cnf(c27,plain,skolem0002!=skolem0003|~in(X158,skolem0004(X157))|skolem0005(X157,X158)=X158,inference(split_conjunct,[status(thm)],[c9])).
% 16.11/16.29 cnf(c16872,plain,skolem0002!=skolem0003|skolem0005(skolem0007,skolem0008(skolem0004(skolem0007)))=skolem0008(skolem0004(skolem0007)),inference(resolution,[status(thm)],[c16852, c27])).
% 16.11/16.29 cnf(c17349,plain,skolem0005(skolem0007,skolem0008(skolem0004(skolem0007)))=skolem0008(skolem0004(skolem0007)),inference(resolution,[status(thm)],[c16872, c16733])).
% 16.11/16.30 cnf(c17363,plain,skolem0007!=X3361|in(skolem0008(skolem0004(skolem0007)),X3361),inference(resolution,[status(thm)],[c17349, c16917])).
% 16.11/16.30 cnf(c17366,plain,in(skolem0008(skolem0004(skolem0007)),skolem0007),inference(resolution,[status(thm)],[c17363, reflexivity])).
% 16.11/16.30 cnf(c17368,plain,~in(skolem0008(skolem0004(skolem0007)),skolem0004(skolem0007))|~ordinal(skolem0008(skolem0004(skolem0007))),inference(resolution,[status(thm)],[c17366, c52])).
% 16.11/16.30 cnf(c17412,plain,~ordinal(skolem0008(skolem0004(skolem0007))),inference(resolution,[status(thm)],[c17368, c16852])).
% 16.11/16.30 cnf(c17414,plain,$false,inference(resolution,[status(thm)],[c17412, c964])).
% 16.11/16.30 % SZS output end CNFRefutation
% 16.11/16.30
% 16.11/16.30 % Initial clauses : 37
% 16.11/16.30 % Processed clauses : 1544
% 16.11/16.30 % Factors computed : 39
% 16.11/16.30 % Resolvents computed: 17322
% 16.11/16.30 % Tautologies deleted: 49
% 16.11/16.30 % Forward subsumed : 3154
% 16.11/16.30 % Backward subsumed : 1259
% 16.11/16.30 % -------- CPU Time ---------
% 16.11/16.30 % User time : 15.898 s
% 16.11/16.30 % System time : 0.050 s
% 16.11/16.30 % Total time : 15.948 s
%------------------------------------------------------------------------------