%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU356+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:10 EDT 2024
% Result : Theorem 100.03s 100.25s
% Output : Refutation 100.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU356+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n008.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 10:53:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 100.03/100.25 % Version: 1.5
% 100.03/100.25 % SZS status Theorem
% 100.03/100.25 % SZS output start CNFRefutation
% 100.03/100.25 fof(t15_yellow_0,conjecture,(![A]:((antisymmetric_relstr(A)&rel_str(A))=>(![B]:(ex_sup_of_relstr_set(A,B)<=>(?[C]:((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]:(element(D,the_carrier(A))=>(relstr_set_smaller(A,B,D)=>related(A,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t15_yellow_0)).
% 100.03/100.25 fof(c12,negated_conjecture,(~(![A]:((antisymmetric_relstr(A)&rel_str(A))=>(![B]:(ex_sup_of_relstr_set(A,B)<=>(?[C]:((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]:(element(D,the_carrier(A))=>(relstr_set_smaller(A,B,D)=>related(A,C,D))))))))))),inference(assume_negation,[status(cth)],[t15_yellow_0])).
% 100.03/100.25 fof(c13,negated_conjecture,(?[A]:((antisymmetric_relstr(A)&rel_str(A))&(?[B]:((~ex_sup_of_relstr_set(A,B)|(![C]:((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]:(element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D)))))))&(ex_sup_of_relstr_set(A,B)|(?[C]:((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]:(~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))))))),inference(fof_nnf,[status(thm)],[c12])).
% 100.03/100.25 fof(c14,negated_conjecture,(?[X5]:((antisymmetric_relstr(X5)&rel_str(X5))&(?[X6]:((~ex_sup_of_relstr_set(X5,X6)|(![X7]:((~element(X7,the_carrier(X5))|~relstr_set_smaller(X5,X6,X7))|(?[X8]:(element(X8,the_carrier(X5))&(relstr_set_smaller(X5,X6,X8)&~related(X5,X7,X8)))))))&(ex_sup_of_relstr_set(X5,X6)|(?[X9]:((element(X9,the_carrier(X5))&relstr_set_smaller(X5,X6,X9))&(![X10]:(~element(X10,the_carrier(X5))|(~relstr_set_smaller(X5,X6,X10)|related(X5,X9,X10))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 100.03/100.25 fof(c16,negated_conjecture,(![X7]:(![X10]:((antisymmetric_relstr(skolem0001)&rel_str(skolem0001))&((~ex_sup_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X7))|(element(skolem0003(X7),the_carrier(skolem0001))&(relstr_set_smaller(skolem0001,skolem0002,skolem0003(X7))&~related(skolem0001,X7,skolem0003(X7))))))&(ex_sup_of_relstr_set(skolem0001,skolem0002)|((element(skolem0004,the_carrier(skolem0001))&relstr_set_smaller(skolem0001,skolem0002,skolem0004))&(~element(X10,the_carrier(skolem0001))|(~relstr_set_smaller(skolem0001,skolem0002,X10)|related(skolem0001,skolem0004,X10))))))))),inference(shift_quantors,[status(thm)],[fof(c15,negated_conjecture,((antisymmetric_relstr(skolem0001)&rel_str(skolem0001))&((~ex_sup_of_relstr_set(skolem0001,skolem0002)|(![X7]:((~element(X7,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X7))|(element(skolem0003(X7),the_carrier(skolem0001))&(relstr_set_smaller(skolem0001,skolem0002,skolem0003(X7))&~related(skolem0001,X7,skolem0003(X7)))))))&(ex_sup_of_relstr_set(skolem0001,skolem0002)|((element(skolem0004,the_carrier(skolem0001))&relstr_set_smaller(skolem0001,skolem0002,skolem0004))&(![X10]:(~element(X10,the_carrier(skolem0001))|(~relstr_set_smaller(skolem0001,skolem0002,X10)|related(skolem0001,skolem0004,X10)))))))),inference(skolemize,[status(esa)],[c14])).])).
% 100.03/100.25 fof(c17,negated_conjecture,(![X7]:(![X10]:((antisymmetric_relstr(skolem0001)&rel_str(skolem0001))&(((~ex_sup_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X7))|element(skolem0003(X7),the_carrier(skolem0001))))&((~ex_sup_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X7))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(X7))))&(~ex_sup_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X7))|~related(skolem0001,X7,skolem0003(X7))))))&(((ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0004,the_carrier(skolem0001)))&(ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0004)))&(ex_sup_of_relstr_set(skolem0001,skolem0002)|(~element(X10,the_carrier(skolem0001))|(~relstr_set_smaller(skolem0001,skolem0002,X10)|related(skolem0001,skolem0004,X10))))))))),inference(distribute,[status(thm)],[c16])).
% 100.03/100.25 cnf(c19,negated_conjecture,rel_str(skolem0001),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.25 cnf(c23,negated_conjecture,ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0004,the_carrier(skolem0001)),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.25 fof(d7_yellow_0,axiom,(![A]:(rel_str(A)=>(![B]:(ex_sup_of_relstr_set(A,B)<=>(?[C]:(((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]:(element(D,the_carrier(A))=>(relstr_set_smaller(A,B,D)=>related(A,C,D)))))&(![D]:(element(D,the_carrier(A))=>((relstr_set_smaller(A,B,D)&(![E]:(element(E,the_carrier(A))=>(relstr_set_smaller(A,B,E)=>related(A,D,E)))))=>D=C))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d7_yellow_0)).
% 100.03/100.25 fof(c41,plain,(![A]:(~rel_str(A)|(![B]:((~ex_sup_of_relstr_set(A,B)|(?[C]:(((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]:(~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))&(![D]:(~element(D,the_carrier(A))|((~relstr_set_smaller(A,B,D)|(?[E]:(element(E,the_carrier(A))&(relstr_set_smaller(A,B,E)&~related(A,D,E)))))|D=C))))))&((![C]:(((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]:(element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D)))))|(?[D]:(element(D,the_carrier(A))&((relstr_set_smaller(A,B,D)&(![E]:(~element(E,the_carrier(A))|(~relstr_set_smaller(A,B,E)|related(A,D,E)))))&D!=C)))))|ex_sup_of_relstr_set(A,B)))))),inference(fof_nnf,[status(thm)],[d7_yellow_0])).
% 100.03/100.25 fof(c42,plain,(![A]:(~rel_str(A)|((![B]:(~ex_sup_of_relstr_set(A,B)|(?[C]:(((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]:(~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))&(![D]:(~element(D,the_carrier(A))|((~relstr_set_smaller(A,B,D)|(?[E]:(element(E,the_carrier(A))&(relstr_set_smaller(A,B,E)&~related(A,D,E)))))|D=C)))))))&(![B]:((![C]:(((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]:(element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D)))))|(?[D]:(element(D,the_carrier(A))&((relstr_set_smaller(A,B,D)&(![E]:(~element(E,the_carrier(A))|(~relstr_set_smaller(A,B,E)|related(A,D,E)))))&D!=C)))))|ex_sup_of_relstr_set(A,B)))))),inference(shift_quantors,[status(thm)],[c41])).
% 100.03/100.25 fof(c43,plain,(![X16]:(~rel_str(X16)|((![X17]:(~ex_sup_of_relstr_set(X16,X17)|(?[X18]:(((element(X18,the_carrier(X16))&relstr_set_smaller(X16,X17,X18))&(![X19]:(~element(X19,the_carrier(X16))|(~relstr_set_smaller(X16,X17,X19)|related(X16,X18,X19)))))&(![X20]:(~element(X20,the_carrier(X16))|((~relstr_set_smaller(X16,X17,X20)|(?[X21]:(element(X21,the_carrier(X16))&(relstr_set_smaller(X16,X17,X21)&~related(X16,X20,X21)))))|X20=X18)))))))&(![X22]:((![X23]:(((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|(?[X24]:(element(X24,the_carrier(X16))&(relstr_set_smaller(X16,X22,X24)&~related(X16,X23,X24)))))|(?[X25]:(element(X25,the_carrier(X16))&((relstr_set_smaller(X16,X22,X25)&(![X26]:(~element(X26,the_carrier(X16))|(~relstr_set_smaller(X16,X22,X26)|related(X16,X25,X26)))))&X25!=X23)))))|ex_sup_of_relstr_set(X16,X22)))))),inference(variable_rename,[status(thm)],[c42])).
% 100.03/100.25 fof(c45,plain,(![X16]:(![X17]:(![X19]:(![X20]:(![X22]:(![X23]:(![X26]:(~rel_str(X16)|((~ex_sup_of_relstr_set(X16,X17)|(((element(skolem0008(X16,X17),the_carrier(X16))&relstr_set_smaller(X16,X17,skolem0008(X16,X17)))&(~element(X19,the_carrier(X16))|(~relstr_set_smaller(X16,X17,X19)|related(X16,skolem0008(X16,X17),X19))))&(~element(X20,the_carrier(X16))|((~relstr_set_smaller(X16,X17,X20)|(element(skolem0009(X16,X17,X20),the_carrier(X16))&(relstr_set_smaller(X16,X17,skolem0009(X16,X17,X20))&~related(X16,X20,skolem0009(X16,X17,X20)))))|X20=skolem0008(X16,X17)))))&((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|(element(skolem0010(X16,X22,X23),the_carrier(X16))&(relstr_set_smaller(X16,X22,skolem0010(X16,X22,X23))&~related(X16,X23,skolem0010(X16,X22,X23)))))|(element(skolem0011(X16,X22,X23),the_carrier(X16))&((relstr_set_smaller(X16,X22,skolem0011(X16,X22,X23))&(~element(X26,the_carrier(X16))|(~relstr_set_smaller(X16,X22,X26)|related(X16,skolem0011(X16,X22,X23),X26))))&skolem0011(X16,X22,X23)!=X23)))|ex_sup_of_relstr_set(X16,X22))))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,(![X16]:(~rel_str(X16)|((![X17]:(~ex_sup_of_relstr_set(X16,X17)|(((element(skolem0008(X16,X17),the_carrier(X16))&relstr_set_smaller(X16,X17,skolem0008(X16,X17)))&(![X19]:(~element(X19,the_carrier(X16))|(~relstr_set_smaller(X16,X17,X19)|related(X16,skolem0008(X16,X17),X19)))))&(![X20]:(~element(X20,the_carrier(X16))|((~relstr_set_smaller(X16,X17,X20)|(element(skolem0009(X16,X17,X20),the_carrier(X16))&(relstr_set_smaller(X16,X17,skolem0009(X16,X17,X20))&~related(X16,X20,skolem0009(X16,X17,X20)))))|X20=skolem0008(X16,X17)))))))&(![X22]:((![X23]:(((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|(element(skolem0010(X16,X22,X23),the_carrier(X16))&(relstr_set_smaller(X16,X22,skolem0010(X16,X22,X23))&~related(X16,X23,skolem0010(X16,X22,X23)))))|(element(skolem0011(X16,X22,X23),the_carrier(X16))&((relstr_set_smaller(X16,X22,skolem0011(X16,X22,X23))&(![X26]:(~element(X26,the_carrier(X16))|(~relstr_set_smaller(X16,X22,X26)|related(X16,skolem0011(X16,X22,X23),X26)))))&skolem0011(X16,X22,X23)!=X23))))|ex_sup_of_relstr_set(X16,X22)))))),inference(skolemize,[status(esa)],[c43])).])).
% 100.03/100.25 fof(c46,plain,(![X16]:(![X17]:(![X19]:(![X20]:(![X22]:(![X23]:(![X26]:(((((~rel_str(X16)|(~ex_sup_of_relstr_set(X16,X17)|element(skolem0008(X16,X17),the_carrier(X16))))&(~rel_str(X16)|(~ex_sup_of_relstr_set(X16,X17)|relstr_set_smaller(X16,X17,skolem0008(X16,X17)))))&(~rel_str(X16)|(~ex_sup_of_relstr_set(X16,X17)|(~element(X19,the_carrier(X16))|(~relstr_set_smaller(X16,X17,X19)|related(X16,skolem0008(X16,X17),X19))))))&((~rel_str(X16)|(~ex_sup_of_relstr_set(X16,X17)|(~element(X20,the_carrier(X16))|((~relstr_set_smaller(X16,X17,X20)|element(skolem0009(X16,X17,X20),the_carrier(X16)))|X20=skolem0008(X16,X17)))))&((~rel_str(X16)|(~ex_sup_of_relstr_set(X16,X17)|(~element(X20,the_carrier(X16))|((~relstr_set_smaller(X16,X17,X20)|relstr_set_smaller(X16,X17,skolem0009(X16,X17,X20)))|X20=skolem0008(X16,X17)))))&(~rel_str(X16)|(~ex_sup_of_relstr_set(X16,X17)|(~element(X20,the_carrier(X16))|((~relstr_set_smaller(X16,X17,X20)|~related(X16,X20,skolem0009(X16,X17,X20)))|X20=skolem0008(X16,X17))))))))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|element(skolem0011(X16,X22,X23),the_carrier(X16)))|ex_sup_of_relstr_set(X16,X22)))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|relstr_set_smaller(X16,X22,skolem0011(X16,X22,X23)))|ex_sup_of_relstr_set(X16,X22)))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|(~element(X26,the_carrier(X16))|(~relstr_set_smaller(X16,X22,X26)|related(X16,skolem0011(X16,X22,X23),X26))))|ex_sup_of_relstr_set(X16,X22))))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|skolem0011(X16,X22,X23)!=X23)|ex_sup_of_relstr_set(X16,X22)))))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|relstr_set_smaller(X16,X22,skolem0010(X16,X22,X23)))|element(skolem0011(X16,X22,X23),the_carrier(X16)))|ex_sup_of_relstr_set(X16,X22)))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|relstr_set_smaller(X16,X22,skolem0010(X16,X22,X23)))|relstr_set_smaller(X16,X22,skolem0011(X16,X22,X23)))|ex_sup_of_relstr_set(X16,X22)))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|relstr_set_smaller(X16,X22,skolem0010(X16,X22,X23)))|(~element(X26,the_carrier(X16))|(~relstr_set_smaller(X16,X22,X26)|related(X16,skolem0011(X16,X22,X23),X26))))|ex_sup_of_relstr_set(X16,X22))))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|relstr_set_smaller(X16,X22,skolem0010(X16,X22,X23)))|skolem0011(X16,X22,X23)!=X23)|ex_sup_of_relstr_set(X16,X22)))))&((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|~related(X16,X23,skolem0010(X16,X22,X23)))|element(skolem0011(X16,X22,X23),the_carrier(X16)))|ex_sup_of_relstr_set(X16,X22)))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|~related(X16,X23,skolem0010(X16,X22,X23)))|relstr_set_smaller(X16,X22,skolem0011(X16,X22,X23)))|ex_sup_of_relstr_set(X16,X22)))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|~related(X16,X23,skolem0010(X16,X22,X23)))|(~element(X26,the_carrier(X16))|(~relstr_set_smaller(X16,X22,X26)|related(X16,skolem0011(X16,X22,X23),X26))))|ex_sup_of_relstr_set(X16,X22))))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_set_smaller(X16,X22,X23))|~related(X16,X23,skolem0010(X16,X22,X23)))|skolem0011(X16,X22,X23)!=X23)|ex_sup_of_relstr_set(X16,X22))))))))))))))),inference(distribute,[status(thm)],[c45])).
% 100.03/100.25 cnf(c47,plain,~rel_str(X67)|~ex_sup_of_relstr_set(X67,X68)|element(skolem0008(X67,X68),the_carrier(X67)),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.25 cnf(c83,plain,~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c47, c23])).
% 100.03/100.25 cnf(c111,plain,element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c83, c19])).
% 100.03/100.25 cnf(c48,plain,~rel_str(X55)|~ex_sup_of_relstr_set(X55,X56)|relstr_set_smaller(X55,X56,skolem0008(X55,X56)),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.25 cnf(c77,plain,~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c48, c23])).
% 100.03/100.25 cnf(c98,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c77, c19])).
% 100.03/100.25 cnf(c22,negated_conjecture,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(X103,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X103)|~related(skolem0001,X103,skolem0003(X103)),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.25 cnf(c20,negated_conjecture,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(X95,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X95)|element(skolem0003(X95),the_carrier(skolem0001)),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.25 cnf(c100,plain,element(skolem0004,the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c98, c20])).
% 100.03/100.25 cnf(c265,plain,element(skolem0004,the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c100, c111])).
% 100.03/100.25 cnf(c269,plain,element(skolem0004,the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c265, c23])).
% 100.03/100.25 cnf(c49,plain,~rel_str(X97)|~ex_sup_of_relstr_set(X97,X98)|~element(X99,the_carrier(X97))|~relstr_set_smaller(X97,X98,X99)|related(X97,skolem0008(X97,X98),X99),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.25 cnf(c21,negated_conjecture,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(X96,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X96)|relstr_set_smaller(skolem0001,skolem0002,skolem0003(X96)),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.25 cnf(c103,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c21, c98])).
% 100.03/100.25 cnf(c274,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c103, c111])).
% 100.03/100.25 cnf(c279,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c274, c23])).
% 100.03/100.25 cnf(c292,plain,element(skolem0004,the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c279, c49])).
% 100.03/100.25 cnf(c1225,plain,element(skolem0004,the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c292, c269])).
% 100.03/100.25 cnf(c1233,plain,element(skolem0004,the_carrier(skolem0001))|~rel_str(skolem0001)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c1225, c23])).
% 100.03/100.25 cnf(c1235,plain,element(skolem0004,the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c1233, c19])).
% 100.03/100.26 cnf(c1241,plain,element(skolem0004,the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1235, c22])).
% 100.03/100.26 cnf(c1248,plain,element(skolem0004,the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c1241, c98])).
% 100.03/100.26 cnf(c1251,plain,element(skolem0004,the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1248, c111])).
% 100.03/100.26 cnf(c1261,plain,element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c1251, c23])).
% 100.03/100.26 cnf(c24,negated_conjecture,ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.26 cnf(c82,plain,~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c47, c24])).
% 100.03/100.26 cnf(c102,plain,element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c82, c19])).
% 100.03/100.26 cnf(c76,plain,~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c48, c24])).
% 100.03/100.26 cnf(c93,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c76, c19])).
% 100.03/100.26 cnf(c95,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c93, c20])).
% 100.03/100.26 cnf(c246,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c95, c102])).
% 100.03/100.26 cnf(c248,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c246, c24])).
% 100.03/100.26 cnf(c106,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c21, c93])).
% 100.03/100.26 cnf(c306,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c106, c102])).
% 100.03/100.26 cnf(c308,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c306, c24])).
% 100.03/100.26 cnf(c322,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c308, c49])).
% 100.03/100.26 cnf(c1468,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c322, c248])).
% 100.03/100.26 cnf(c1474,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~rel_str(skolem0001)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c1468, c24])).
% 100.03/100.26 cnf(c1476,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c1474, c19])).
% 100.03/100.26 cnf(c1492,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1476, c22])).
% 100.03/100.26 cnf(c1498,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c1492, c93])).
% 100.03/100.26 cnf(c1507,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1498, c102])).
% 100.03/100.26 cnf(c1515,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c1507, c24])).
% 100.03/100.26 cnf(c64,plain,~rel_str(X229)|~element(X230,the_carrier(X229))|~relstr_set_smaller(X229,X228,X230)|~related(X229,X230,skolem0010(X229,X228,X230))|skolem0011(X229,X228,X230)!=X230|ex_sup_of_relstr_set(X229,X228),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c25,negated_conjecture,ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(X107,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X107)|related(skolem0001,skolem0004,X107),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.26 cnf(c60,plain,~rel_str(X195)|~element(X196,the_carrier(X195))|~relstr_set_smaller(X195,X194,X196)|relstr_set_smaller(X195,X194,skolem0010(X195,X194,X196))|skolem0011(X195,X194,X196)!=X196|ex_sup_of_relstr_set(X195,X194),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(symmetry,axiom,X28!=X29|X29=X28,theory(equality)).
% 100.03/100.26 cnf(c18,negated_conjecture,antisymmetric_relstr(skolem0001),inference(split_conjunct,[status(thm)],[c17])).
% 100.03/100.26 cnf(c61,plain,~rel_str(X204)|~element(X205,the_carrier(X204))|~relstr_set_smaller(X204,X203,X205)|~related(X204,X205,skolem0010(X204,X203,X205))|element(skolem0011(X204,X203,X205),the_carrier(X204))|ex_sup_of_relstr_set(X204,X203),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c53,plain,~rel_str(X129)|~element(X130,the_carrier(X129))|~relstr_set_smaller(X129,X128,X130)|element(skolem0010(X129,X128,X130),the_carrier(X129))|element(skolem0011(X129,X128,X130),the_carrier(X129))|ex_sup_of_relstr_set(X129,X128),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c170,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c53, c24])).
% 100.03/100.26 cnf(c617,plain,~rel_str(skolem0001)|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c170, c23])).
% 100.03/100.26 cnf(c626,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c617, c19])).
% 100.03/100.26 cnf(c57,plain,~rel_str(X163)|~element(X164,the_carrier(X163))|~relstr_set_smaller(X163,X162,X164)|relstr_set_smaller(X163,X162,skolem0010(X163,X162,X164))|element(skolem0011(X163,X162,X164),the_carrier(X163))|ex_sup_of_relstr_set(X163,X162),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c201,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c57, c24])).
% 100.03/100.26 cnf(c779,plain,~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c201, c23])).
% 100.03/100.26 cnf(c781,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c779, c19])).
% 100.03/100.26 cnf(c796,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0010(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c781, c25])).
% 100.03/100.26 cnf(c2748,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0004,skolem0010(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c796, c626])).
% 100.03/100.26 cnf(c2774,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c2748, c61])).
% 100.03/100.26 cnf(c2806,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2774, c1515])).
% 100.03/100.26 cnf(c2807,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c2806, c1261])).
% 100.03/100.26 cnf(c2808,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2807, c19])).
% 100.03/100.26 cnf(c2810,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2808, c47])).
% 100.03/100.26 cnf(c2841,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2810, c19])).
% 100.03/100.26 cnf(c2812,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c2808, c48])).
% 100.03/100.26 cnf(c2844,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c2812, c19])).
% 100.03/100.26 cnf(c2858,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2844, c20])).
% 100.03/100.26 cnf(c3371,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2858, c2841])).
% 100.03/100.26 cnf(c3379,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c3371, c2808])).
% 100.03/100.26 cnf(c2851,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c2844, c21])).
% 100.03/100.26 cnf(c3338,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c2851, c2841])).
% 100.03/100.26 cnf(c3346,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c3338, c2808])).
% 100.03/100.26 cnf(c3364,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c3346, c49])).
% 100.03/100.26 cnf(c14112,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c3364, c3379])).
% 100.03/100.26 cnf(c14116,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c14112, c2808])).
% 100.03/100.26 cnf(c14120,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c14116, c19])).
% 100.03/100.26 cnf(c14138,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c14120, c22])).
% 100.03/100.26 cnf(c14146,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c14138, c2844])).
% 100.03/100.26 cnf(c14151,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c14146, c2841])).
% 100.03/100.26 cnf(c14157,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c14151, c2808])).
% 100.03/100.26 cnf(c62,plain,~rel_str(X215)|~element(X216,the_carrier(X215))|~relstr_set_smaller(X215,X214,X216)|~related(X215,X216,skolem0010(X215,X214,X216))|relstr_set_smaller(X215,X214,skolem0011(X215,X214,X216))|ex_sup_of_relstr_set(X215,X214),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c54,plain,~rel_str(X138)|~element(X139,the_carrier(X138))|~relstr_set_smaller(X138,X137,X139)|element(skolem0010(X138,X137,X139),the_carrier(X138))|relstr_set_smaller(X138,X137,skolem0011(X138,X137,X139))|ex_sup_of_relstr_set(X138,X137),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c179,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c54, c24])).
% 100.03/100.26 cnf(c670,plain,~rel_str(skolem0001)|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c179, c23])).
% 100.03/100.26 cnf(c672,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c670, c19])).
% 100.03/100.26 cnf(c58,plain,~rel_str(X173)|~element(X174,the_carrier(X173))|~relstr_set_smaller(X173,X172,X174)|relstr_set_smaller(X173,X172,skolem0010(X173,X172,X174))|relstr_set_smaller(X173,X172,skolem0011(X173,X172,X174))|ex_sup_of_relstr_set(X173,X172),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c211,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c58, c24])).
% 100.03/100.26 cnf(c887,plain,~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c211, c23])).
% 100.03/100.26 cnf(c893,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c887, c19])).
% 100.03/100.26 cnf(c908,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0010(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c893, c25])).
% 100.03/100.26 cnf(c3794,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0004,skolem0010(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c908, c672])).
% 100.03/100.26 cnf(c3835,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c3794, c62])).
% 100.03/100.26 cnf(c3897,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c3835, c1515])).
% 100.03/100.26 cnf(c3898,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c3897, c1261])).
% 100.03/100.26 cnf(c3899,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c3898, c19])).
% 100.03/100.26 cnf(c3914,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c3899, c25])).
% 100.03/100.26 cnf(c4044,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c3914, c2808])).
% 100.03/100.26 fof(t25_orders_2,axiom,(![A]:((antisymmetric_relstr(A)&rel_str(A))=>(![B]:(element(B,the_carrier(A))=>(![C]:(element(C,the_carrier(A))=>((related(A,B,C)&related(A,C,B))=>B=C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t25_orders_2)).
% 100.03/100.26 fof(c8,plain,(![A]:((~antisymmetric_relstr(A)|~rel_str(A))|(![B]:(~element(B,the_carrier(A))|(![C]:(~element(C,the_carrier(A))|((~related(A,B,C)|~related(A,C,B))|B=C))))))),inference(fof_nnf,[status(thm)],[t25_orders_2])).
% 100.03/100.26 fof(c10,plain,(![X2]:(![X3]:(![X4]:((~antisymmetric_relstr(X2)|~rel_str(X2))|(~element(X3,the_carrier(X2))|(~element(X4,the_carrier(X2))|((~related(X2,X3,X4)|~related(X2,X4,X3))|X3=X4))))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,(![X2]:((~antisymmetric_relstr(X2)|~rel_str(X2))|(![X3]:(~element(X3,the_carrier(X2))|(![X4]:(~element(X4,the_carrier(X2))|((~related(X2,X3,X4)|~related(X2,X4,X3))|X3=X4))))))),inference(variable_rename,[status(thm)],[c8])).])).
% 100.03/100.26 cnf(c11,plain,~antisymmetric_relstr(X89)|~rel_str(X89)|~element(X88,the_carrier(X89))|~element(X87,the_carrier(X89))|~related(X89,X88,X87)|~related(X89,X87,X88)|X88=X87,inference(split_conjunct,[status(thm)],[c10])).
% 100.03/100.26 cnf(c59,plain,~rel_str(X182)|~element(X183,the_carrier(X182))|~relstr_set_smaller(X182,X181,X183)|relstr_set_smaller(X182,X181,skolem0010(X182,X181,X183))|~element(X184,the_carrier(X182))|~relstr_set_smaller(X182,X181,X184)|related(X182,skolem0011(X182,X181,X183),X184)|ex_sup_of_relstr_set(X182,X181),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c216,plain,~rel_str(X270)|~element(X272,the_carrier(X270))|~relstr_set_smaller(X270,X271,X272)|relstr_set_smaller(X270,X271,skolem0010(X270,X271,X272))|related(X270,skolem0011(X270,X271,X272),X272)|ex_sup_of_relstr_set(X270,X271),inference(factor,[status(thm)],[c59])).
% 100.03/100.26 cnf(c412,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c216, c24])).
% 100.03/100.26 cnf(c1980,plain,~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c412, c1261])).
% 100.03/100.26 cnf(c1992,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1980, c19])).
% 100.03/100.26 cnf(c2009,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c1992, c11])).
% 100.03/100.26 cnf(c13591,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c2009, c4044])).
% 100.03/100.26 cnf(c18007,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c13591, c14157])).
% 100.03/100.26 cnf(c18008,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c18007, c1261])).
% 100.03/100.26 cnf(c18009,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c18008, c19])).
% 100.03/100.26 cnf(c18010,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c18009, c18])).
% 100.03/100.26 cnf(c18069,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c18010, symmetry])).
% 100.03/100.26 cnf(c18238,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c18069, c60])).
% 100.03/100.26 cnf(c19108,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c18238, c1515])).
% 100.03/100.26 cnf(c19109,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c19108, c1261])).
% 100.03/100.26 cnf(c19110,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c19109, c19])).
% 100.03/100.26 cnf(c19116,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0010(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c19110, c25])).
% 100.03/100.26 cnf(c56,plain,~rel_str(X155)|~element(X156,the_carrier(X155))|~relstr_set_smaller(X155,X154,X156)|element(skolem0010(X155,X154,X156),the_carrier(X155))|skolem0011(X155,X154,X156)!=X156|ex_sup_of_relstr_set(X155,X154),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c4076,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4044, c47])).
% 100.03/100.26 cnf(c4108,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4076, c19])).
% 100.03/100.26 cnf(c4078,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c4044, c48])).
% 100.03/100.26 cnf(c4112,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c4078, c19])).
% 100.03/100.26 cnf(c4127,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4112, c20])).
% 100.03/100.26 cnf(c5671,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4127, c4108])).
% 100.03/100.26 cnf(c5677,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c5671, c4044])).
% 100.03/100.26 cnf(c4120,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c4112, c21])).
% 100.03/100.26 cnf(c5631,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c4120, c4108])).
% 100.03/100.26 cnf(c5637,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c5631, c4044])).
% 100.03/100.26 cnf(c5654,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c5637, c49])).
% 100.03/100.26 cnf(c14671,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c5654, c5677])).
% 100.03/100.26 cnf(c14673,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~rel_str(skolem0001)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c14671, c4044])).
% 100.03/100.26 cnf(c14676,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c14673, c19])).
% 100.03/100.26 cnf(c14682,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c14676, c22])).
% 100.03/100.26 cnf(c14693,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c14682, c4112])).
% 100.03/100.26 cnf(c14697,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|~ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c14693, c4108])).
% 100.03/100.26 cnf(c14701,plain,related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c14697, c4044])).
% 100.03/100.26 cnf(c55,plain,~rel_str(X145)|~element(X146,the_carrier(X145))|~relstr_set_smaller(X145,X144,X146)|element(skolem0010(X145,X144,X146),the_carrier(X145))|~element(X147,the_carrier(X145))|~relstr_set_smaller(X145,X144,X147)|related(X145,skolem0011(X145,X144,X146),X147)|ex_sup_of_relstr_set(X145,X144),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c184,plain,~rel_str(X297)|~element(X299,the_carrier(X297))|~relstr_set_smaller(X297,X298,X299)|element(skolem0010(X297,X298,X299),the_carrier(X297))|related(X297,skolem0011(X297,X298,X299),X299)|ex_sup_of_relstr_set(X297,X298),inference(factor,[status(thm)],[c55])).
% 100.03/100.26 cnf(c436,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c184, c24])).
% 100.03/100.26 cnf(c2227,plain,~rel_str(skolem0001)|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c436, c1261])).
% 100.03/100.26 cnf(c2228,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2227, c19])).
% 100.03/100.26 cnf(c2231,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c2228, c11])).
% 100.03/100.26 cnf(c15071,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c2231, c14701])).
% 100.03/100.26 cnf(c29362,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c15071, c14157])).
% 100.03/100.26 cnf(c29363,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c29362, c1261])).
% 100.03/100.26 cnf(c29364,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c29363, c19])).
% 100.03/100.26 cnf(c29365,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c29364, c18])).
% 100.03/100.26 cnf(c29462,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c29365, symmetry])).
% 100.03/100.26 cnf(c29841,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c29462, c56])).
% 100.03/100.26 cnf(c32297,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c29841, c1515])).
% 100.03/100.26 cnf(c32298,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c32297, c1261])).
% 100.03/100.26 cnf(c32299,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c32298, c19])).
% 100.03/100.26 cnf(c32309,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0004,skolem0010(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c32299, c19116])).
% 100.03/100.26 cnf(c32447,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004)|skolem0011(skolem0001,skolem0002,skolem0004)!=skolem0004,inference(resolution,[status(thm)],[c32309, c64])).
% 100.03/100.26 cnf(c14708,plain,~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~element(skolem0004,the_carrier(skolem0001))|~related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c14701, c11])).
% 100.03/100.26 cnf(c63,plain,~rel_str(X225)|~element(X226,the_carrier(X225))|~relstr_set_smaller(X225,X224,X226)|~related(X225,X226,skolem0010(X225,X224,X226))|~element(X227,the_carrier(X225))|~relstr_set_smaller(X225,X224,X227)|related(X225,skolem0011(X225,X224,X226),X227)|ex_sup_of_relstr_set(X225,X224),inference(split_conjunct,[status(thm)],[c46])).
% 100.03/100.26 cnf(c32451,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004)|~element(X7777,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,X7777)|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),X7777),inference(resolution,[status(thm)],[c32309, c63])).
% 100.03/100.26 cnf(c38622,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004)|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(factor,[status(thm)],[c32451])).
% 100.03/100.26 cnf(c38696,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c38622, c1515])).
% 100.03/100.26 cnf(c38697,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c38696, c1261])).
% 100.03/100.26 cnf(c38698,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c38697, c19])).
% 100.03/100.26 cnf(c38771,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~element(skolem0004,the_carrier(skolem0001))|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c38698, c14708])).
% 100.03/100.26 cnf(c40487,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c38771, c14157])).
% 100.03/100.26 cnf(c40488,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c40487, c1261])).
% 100.03/100.26 cnf(c40489,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c40488, c19])).
% 100.03/100.26 cnf(c40490,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c40489, c18])).
% 100.03/100.26 cnf(c40574,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c40490, c32447])).
% 100.03/100.26 cnf(c41480,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c40574, c1515])).
% 100.03/100.26 cnf(c41481,plain,ex_sup_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c41480, c1261])).
% 100.03/100.26 cnf(c41482,plain,ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c41481, c19])).
% 100.03/100.26 cnf(c41497,plain,~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c41482, c47])).
% 100.03/100.26 cnf(c41589,plain,element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c41497, c19])).
% 100.03/100.26 cnf(c41486,plain,~rel_str(skolem0001)|relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c41482, c48])).
% 100.03/100.26 cnf(c41574,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c41486, c19])).
% 100.03/100.26 cnf(c41588,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c41574, c20])).
% 100.03/100.26 cnf(c42504,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c41588, c41589])).
% 100.03/100.26 cnf(c42505,plain,element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c42504, c41482])).
% 100.03/100.26 cnf(c41576,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c41574, c21])).
% 100.03/100.26 cnf(c42485,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c41576, c41589])).
% 100.03/100.26 cnf(c42486,plain,relstr_set_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c42485, c41482])).
% 100.03/100.26 cnf(c42496,plain,~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c42486, c49])).
% 100.03/100.26 cnf(c43271,plain,~rel_str(skolem0001)|~ex_sup_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c42496, c42505])).
% 100.03/100.26 cnf(c43272,plain,~rel_str(skolem0001)|related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c43271, c41482])).
% 100.03/100.26 cnf(c43273,plain,related(skolem0001,skolem0008(skolem0001,skolem0002),skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c43272, c19])).
% 100.03/100.26 cnf(c43274,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_set_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c43273, c22])).
% 100.03/100.26 cnf(c43277,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c43274, c41574])).
% 100.03/100.26 cnf(c43278,plain,~ex_sup_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c43277, c41589])).
% 100.03/100.26 cnf(c43279,plain,$false,inference(resolution,[status(thm)],[c43278, c41482])).
% 100.03/100.26 % SZS output end CNFRefutation
% 100.03/100.26
% 100.03/100.26 % Initial clauses : 45
% 100.03/100.26 % Processed clauses : 5566
% 100.03/100.26 % Factors computed : 68
% 100.03/100.26 % Resolvents computed: 43147
% 100.03/100.26 % Tautologies deleted: 255
% 100.03/100.26 % Forward subsumed : 10401
% 100.03/100.26 % Backward subsumed : 5334
% 100.03/100.26 % -------- CPU Time ---------
% 100.03/100.26 % User time : 99.773 s
% 100.03/100.26 % System time : 0.147 s
% 100.03/100.26 % Total time : 99.920 s
%------------------------------------------------------------------------------