%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU357+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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 95.80s 95.96s
% Output : Refutation 95.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU357+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n005.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 12:06:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 95.80/95.96 % Version: 1.5
% 95.80/95.96 % SZS status Theorem
% 95.80/95.96 % SZS output start CNFRefutation
% 95.80/95.96 fof(t16_yellow_0,conjecture,(![A]:((antisymmetric_relstr(A)&rel_str(A))=>(![B]:(ex_inf_of_relstr_set(A,B)<=>(?[C]:((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]:(element(D,the_carrier(A))=>(relstr_element_smaller(A,B,D)=>related(A,D,C)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t16_yellow_0)).
% 95.80/95.96 fof(c12,negated_conjecture,(~(![A]:((antisymmetric_relstr(A)&rel_str(A))=>(![B]:(ex_inf_of_relstr_set(A,B)<=>(?[C]:((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]:(element(D,the_carrier(A))=>(relstr_element_smaller(A,B,D)=>related(A,D,C))))))))))),inference(assume_negation,[status(cth)],[t16_yellow_0])).
% 95.80/95.96 fof(c13,negated_conjecture,(?[A]:((antisymmetric_relstr(A)&rel_str(A))&(?[B]:((~ex_inf_of_relstr_set(A,B)|(![C]:((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(?[D]:(element(D,the_carrier(A))&(relstr_element_smaller(A,B,D)&~related(A,D,C)))))))&(ex_inf_of_relstr_set(A,B)|(?[C]:((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]:(~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C))))))))))),inference(fof_nnf,[status(thm)],[c12])).
% 95.80/95.96 fof(c14,negated_conjecture,(?[X5]:((antisymmetric_relstr(X5)&rel_str(X5))&(?[X6]:((~ex_inf_of_relstr_set(X5,X6)|(![X7]:((~element(X7,the_carrier(X5))|~relstr_element_smaller(X5,X6,X7))|(?[X8]:(element(X8,the_carrier(X5))&(relstr_element_smaller(X5,X6,X8)&~related(X5,X8,X7)))))))&(ex_inf_of_relstr_set(X5,X6)|(?[X9]:((element(X9,the_carrier(X5))&relstr_element_smaller(X5,X6,X9))&(![X10]:(~element(X10,the_carrier(X5))|(~relstr_element_smaller(X5,X6,X10)|related(X5,X10,X9))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 95.80/95.96 fof(c16,negated_conjecture,(![X7]:(![X10]:((antisymmetric_relstr(skolem0001)&rel_str(skolem0001))&((~ex_inf_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X7))|(element(skolem0003(X7),the_carrier(skolem0001))&(relstr_element_smaller(skolem0001,skolem0002,skolem0003(X7))&~related(skolem0001,skolem0003(X7),X7)))))&(ex_inf_of_relstr_set(skolem0001,skolem0002)|((element(skolem0004,the_carrier(skolem0001))&relstr_element_smaller(skolem0001,skolem0002,skolem0004))&(~element(X10,the_carrier(skolem0001))|(~relstr_element_smaller(skolem0001,skolem0002,X10)|related(skolem0001,X10,skolem0004))))))))),inference(shift_quantors,[status(thm)],[fof(c15,negated_conjecture,((antisymmetric_relstr(skolem0001)&rel_str(skolem0001))&((~ex_inf_of_relstr_set(skolem0001,skolem0002)|(![X7]:((~element(X7,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X7))|(element(skolem0003(X7),the_carrier(skolem0001))&(relstr_element_smaller(skolem0001,skolem0002,skolem0003(X7))&~related(skolem0001,skolem0003(X7),X7))))))&(ex_inf_of_relstr_set(skolem0001,skolem0002)|((element(skolem0004,the_carrier(skolem0001))&relstr_element_smaller(skolem0001,skolem0002,skolem0004))&(![X10]:(~element(X10,the_carrier(skolem0001))|(~relstr_element_smaller(skolem0001,skolem0002,X10)|related(skolem0001,X10,skolem0004)))))))),inference(skolemize,[status(esa)],[c14])).])).
% 95.80/95.96 fof(c17,negated_conjecture,(![X7]:(![X10]:((antisymmetric_relstr(skolem0001)&rel_str(skolem0001))&(((~ex_inf_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X7))|element(skolem0003(X7),the_carrier(skolem0001))))&((~ex_inf_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X7))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(X7))))&(~ex_inf_of_relstr_set(skolem0001,skolem0002)|((~element(X7,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X7))|~related(skolem0001,skolem0003(X7),X7)))))&(((ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0004,the_carrier(skolem0001)))&(ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0004)))&(ex_inf_of_relstr_set(skolem0001,skolem0002)|(~element(X10,the_carrier(skolem0001))|(~relstr_element_smaller(skolem0001,skolem0002,X10)|related(skolem0001,X10,skolem0004))))))))),inference(distribute,[status(thm)],[c16])).
% 95.80/95.96 cnf(c19,negated_conjecture,rel_str(skolem0001),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c23,negated_conjecture,ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0004,the_carrier(skolem0001)),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 fof(d8_yellow_0,axiom,(![A]:(rel_str(A)=>(![B]:(ex_inf_of_relstr_set(A,B)<=>(?[C]:(((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]:(element(D,the_carrier(A))=>(relstr_element_smaller(A,B,D)=>related(A,D,C)))))&(![D]:(element(D,the_carrier(A))=>((relstr_element_smaller(A,B,D)&(![E]:(element(E,the_carrier(A))=>(relstr_element_smaller(A,B,E)=>related(A,E,D)))))=>D=C))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d8_yellow_0)).
% 95.80/95.96 fof(c41,plain,(![A]:(~rel_str(A)|(![B]:((~ex_inf_of_relstr_set(A,B)|(?[C]:(((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]:(~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C)))))&(![D]:(~element(D,the_carrier(A))|((~relstr_element_smaller(A,B,D)|(?[E]:(element(E,the_carrier(A))&(relstr_element_smaller(A,B,E)&~related(A,E,D)))))|D=C))))))&((![C]:(((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(?[D]:(element(D,the_carrier(A))&(relstr_element_smaller(A,B,D)&~related(A,D,C)))))|(?[D]:(element(D,the_carrier(A))&((relstr_element_smaller(A,B,D)&(![E]:(~element(E,the_carrier(A))|(~relstr_element_smaller(A,B,E)|related(A,E,D)))))&D!=C)))))|ex_inf_of_relstr_set(A,B)))))),inference(fof_nnf,[status(thm)],[d8_yellow_0])).
% 95.80/95.96 fof(c42,plain,(![A]:(~rel_str(A)|((![B]:(~ex_inf_of_relstr_set(A,B)|(?[C]:(((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]:(~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C)))))&(![D]:(~element(D,the_carrier(A))|((~relstr_element_smaller(A,B,D)|(?[E]:(element(E,the_carrier(A))&(relstr_element_smaller(A,B,E)&~related(A,E,D)))))|D=C)))))))&(![B]:((![C]:(((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(?[D]:(element(D,the_carrier(A))&(relstr_element_smaller(A,B,D)&~related(A,D,C)))))|(?[D]:(element(D,the_carrier(A))&((relstr_element_smaller(A,B,D)&(![E]:(~element(E,the_carrier(A))|(~relstr_element_smaller(A,B,E)|related(A,E,D)))))&D!=C)))))|ex_inf_of_relstr_set(A,B)))))),inference(shift_quantors,[status(thm)],[c41])).
% 95.80/95.96 fof(c43,plain,(![X16]:(~rel_str(X16)|((![X17]:(~ex_inf_of_relstr_set(X16,X17)|(?[X18]:(((element(X18,the_carrier(X16))&relstr_element_smaller(X16,X17,X18))&(![X19]:(~element(X19,the_carrier(X16))|(~relstr_element_smaller(X16,X17,X19)|related(X16,X19,X18)))))&(![X20]:(~element(X20,the_carrier(X16))|((~relstr_element_smaller(X16,X17,X20)|(?[X21]:(element(X21,the_carrier(X16))&(relstr_element_smaller(X16,X17,X21)&~related(X16,X21,X20)))))|X20=X18)))))))&(![X22]:((![X23]:(((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|(?[X24]:(element(X24,the_carrier(X16))&(relstr_element_smaller(X16,X22,X24)&~related(X16,X24,X23)))))|(?[X25]:(element(X25,the_carrier(X16))&((relstr_element_smaller(X16,X22,X25)&(![X26]:(~element(X26,the_carrier(X16))|(~relstr_element_smaller(X16,X22,X26)|related(X16,X26,X25)))))&X25!=X23)))))|ex_inf_of_relstr_set(X16,X22)))))),inference(variable_rename,[status(thm)],[c42])).
% 95.80/95.96 fof(c45,plain,(![X16]:(![X17]:(![X19]:(![X20]:(![X22]:(![X23]:(![X26]:(~rel_str(X16)|((~ex_inf_of_relstr_set(X16,X17)|(((element(skolem0008(X16,X17),the_carrier(X16))&relstr_element_smaller(X16,X17,skolem0008(X16,X17)))&(~element(X19,the_carrier(X16))|(~relstr_element_smaller(X16,X17,X19)|related(X16,X19,skolem0008(X16,X17)))))&(~element(X20,the_carrier(X16))|((~relstr_element_smaller(X16,X17,X20)|(element(skolem0009(X16,X17,X20),the_carrier(X16))&(relstr_element_smaller(X16,X17,skolem0009(X16,X17,X20))&~related(X16,skolem0009(X16,X17,X20),X20))))|X20=skolem0008(X16,X17)))))&((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|(element(skolem0010(X16,X22,X23),the_carrier(X16))&(relstr_element_smaller(X16,X22,skolem0010(X16,X22,X23))&~related(X16,skolem0010(X16,X22,X23),X23))))|(element(skolem0011(X16,X22,X23),the_carrier(X16))&((relstr_element_smaller(X16,X22,skolem0011(X16,X22,X23))&(~element(X26,the_carrier(X16))|(~relstr_element_smaller(X16,X22,X26)|related(X16,X26,skolem0011(X16,X22,X23)))))&skolem0011(X16,X22,X23)!=X23)))|ex_inf_of_relstr_set(X16,X22))))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,(![X16]:(~rel_str(X16)|((![X17]:(~ex_inf_of_relstr_set(X16,X17)|(((element(skolem0008(X16,X17),the_carrier(X16))&relstr_element_smaller(X16,X17,skolem0008(X16,X17)))&(![X19]:(~element(X19,the_carrier(X16))|(~relstr_element_smaller(X16,X17,X19)|related(X16,X19,skolem0008(X16,X17))))))&(![X20]:(~element(X20,the_carrier(X16))|((~relstr_element_smaller(X16,X17,X20)|(element(skolem0009(X16,X17,X20),the_carrier(X16))&(relstr_element_smaller(X16,X17,skolem0009(X16,X17,X20))&~related(X16,skolem0009(X16,X17,X20),X20))))|X20=skolem0008(X16,X17)))))))&(![X22]:((![X23]:(((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|(element(skolem0010(X16,X22,X23),the_carrier(X16))&(relstr_element_smaller(X16,X22,skolem0010(X16,X22,X23))&~related(X16,skolem0010(X16,X22,X23),X23))))|(element(skolem0011(X16,X22,X23),the_carrier(X16))&((relstr_element_smaller(X16,X22,skolem0011(X16,X22,X23))&(![X26]:(~element(X26,the_carrier(X16))|(~relstr_element_smaller(X16,X22,X26)|related(X16,X26,skolem0011(X16,X22,X23))))))&skolem0011(X16,X22,X23)!=X23))))|ex_inf_of_relstr_set(X16,X22)))))),inference(skolemize,[status(esa)],[c43])).])).
% 95.80/95.96 fof(c46,plain,(![X16]:(![X17]:(![X19]:(![X20]:(![X22]:(![X23]:(![X26]:(((((~rel_str(X16)|(~ex_inf_of_relstr_set(X16,X17)|element(skolem0008(X16,X17),the_carrier(X16))))&(~rel_str(X16)|(~ex_inf_of_relstr_set(X16,X17)|relstr_element_smaller(X16,X17,skolem0008(X16,X17)))))&(~rel_str(X16)|(~ex_inf_of_relstr_set(X16,X17)|(~element(X19,the_carrier(X16))|(~relstr_element_smaller(X16,X17,X19)|related(X16,X19,skolem0008(X16,X17)))))))&((~rel_str(X16)|(~ex_inf_of_relstr_set(X16,X17)|(~element(X20,the_carrier(X16))|((~relstr_element_smaller(X16,X17,X20)|element(skolem0009(X16,X17,X20),the_carrier(X16)))|X20=skolem0008(X16,X17)))))&((~rel_str(X16)|(~ex_inf_of_relstr_set(X16,X17)|(~element(X20,the_carrier(X16))|((~relstr_element_smaller(X16,X17,X20)|relstr_element_smaller(X16,X17,skolem0009(X16,X17,X20)))|X20=skolem0008(X16,X17)))))&(~rel_str(X16)|(~ex_inf_of_relstr_set(X16,X17)|(~element(X20,the_carrier(X16))|((~relstr_element_smaller(X16,X17,X20)|~related(X16,skolem0009(X16,X17,X20),X20))|X20=skolem0008(X16,X17))))))))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|element(skolem0011(X16,X22,X23),the_carrier(X16)))|ex_inf_of_relstr_set(X16,X22)))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|relstr_element_smaller(X16,X22,skolem0011(X16,X22,X23)))|ex_inf_of_relstr_set(X16,X22)))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|(~element(X26,the_carrier(X16))|(~relstr_element_smaller(X16,X22,X26)|related(X16,X26,skolem0011(X16,X22,X23)))))|ex_inf_of_relstr_set(X16,X22))))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|element(skolem0010(X16,X22,X23),the_carrier(X16)))|skolem0011(X16,X22,X23)!=X23)|ex_inf_of_relstr_set(X16,X22)))))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|relstr_element_smaller(X16,X22,skolem0010(X16,X22,X23)))|element(skolem0011(X16,X22,X23),the_carrier(X16)))|ex_inf_of_relstr_set(X16,X22)))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|relstr_element_smaller(X16,X22,skolem0010(X16,X22,X23)))|relstr_element_smaller(X16,X22,skolem0011(X16,X22,X23)))|ex_inf_of_relstr_set(X16,X22)))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|relstr_element_smaller(X16,X22,skolem0010(X16,X22,X23)))|(~element(X26,the_carrier(X16))|(~relstr_element_smaller(X16,X22,X26)|related(X16,X26,skolem0011(X16,X22,X23)))))|ex_inf_of_relstr_set(X16,X22))))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|relstr_element_smaller(X16,X22,skolem0010(X16,X22,X23)))|skolem0011(X16,X22,X23)!=X23)|ex_inf_of_relstr_set(X16,X22)))))&((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|~related(X16,skolem0010(X16,X22,X23),X23))|element(skolem0011(X16,X22,X23),the_carrier(X16)))|ex_inf_of_relstr_set(X16,X22)))&(((~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|~related(X16,skolem0010(X16,X22,X23),X23))|relstr_element_smaller(X16,X22,skolem0011(X16,X22,X23)))|ex_inf_of_relstr_set(X16,X22)))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|~related(X16,skolem0010(X16,X22,X23),X23))|(~element(X26,the_carrier(X16))|(~relstr_element_smaller(X16,X22,X26)|related(X16,X26,skolem0011(X16,X22,X23)))))|ex_inf_of_relstr_set(X16,X22))))&(~rel_str(X16)|((((~element(X23,the_carrier(X16))|~relstr_element_smaller(X16,X22,X23))|~related(X16,skolem0010(X16,X22,X23),X23))|skolem0011(X16,X22,X23)!=X23)|ex_inf_of_relstr_set(X16,X22))))))))))))))),inference(distribute,[status(thm)],[c45])).
% 95.80/95.96 cnf(c47,plain,~rel_str(X67)|~ex_inf_of_relstr_set(X67,X68)|element(skolem0008(X67,X68),the_carrier(X67)),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c83,plain,~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c47, c23])).
% 95.80/95.96 cnf(c111,plain,element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c83, c19])).
% 95.80/95.96 cnf(c48,plain,~rel_str(X55)|~ex_inf_of_relstr_set(X55,X56)|relstr_element_smaller(X55,X56,skolem0008(X55,X56)),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c77,plain,~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c48, c23])).
% 95.80/95.96 cnf(c98,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c77, c19])).
% 95.80/95.96 cnf(c22,negated_conjecture,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(X103,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X103)|~related(skolem0001,skolem0003(X103),X103),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c20,negated_conjecture,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(X95,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X95)|element(skolem0003(X95),the_carrier(skolem0001)),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c100,plain,element(skolem0004,the_carrier(skolem0001))|~ex_inf_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])).
% 95.80/95.96 cnf(c267,plain,element(skolem0004,the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c100, c111])).
% 95.80/95.96 cnf(c269,plain,element(skolem0004,the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c267, c23])).
% 95.80/95.96 cnf(c49,plain,~rel_str(X97)|~ex_inf_of_relstr_set(X97,X98)|~element(X99,the_carrier(X97))|~relstr_element_smaller(X97,X98,X99)|related(X97,X99,skolem0008(X97,X98)),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c21,negated_conjecture,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(X96,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X96)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(X96)),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c106,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c21, c98])).
% 95.80/95.96 cnf(c318,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c106, c111])).
% 95.80/95.96 cnf(c320,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c318, c23])).
% 95.80/95.96 cnf(c333,plain,element(skolem0004,the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c320, c49])).
% 95.80/95.96 cnf(c1475,plain,element(skolem0004,the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c333, c269])).
% 95.80/95.96 cnf(c1480,plain,element(skolem0004,the_carrier(skolem0001))|~rel_str(skolem0001)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1475, c23])).
% 95.80/95.96 cnf(c1482,plain,element(skolem0004,the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1480, c19])).
% 95.80/95.96 cnf(c1491,plain,element(skolem0004,the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1482, c22])).
% 95.80/95.96 cnf(c1537,plain,element(skolem0004,the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c1491, c98])).
% 95.80/95.96 cnf(c1540,plain,element(skolem0004,the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1537, c111])).
% 95.80/95.96 cnf(c1548,plain,element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c1540, c23])).
% 95.80/95.96 cnf(c24,negated_conjecture,ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c82,plain,~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c47, c24])).
% 95.80/95.96 cnf(c102,plain,element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c82, c19])).
% 95.80/95.96 cnf(c76,plain,~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c48, c24])).
% 95.80/95.96 cnf(c93,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c76, c19])).
% 95.80/95.96 cnf(c95,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~ex_inf_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])).
% 95.80/95.96 cnf(c246,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c95, c102])).
% 95.80/95.96 cnf(c248,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c246, c24])).
% 95.80/95.96 cnf(c105,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c21, c93])).
% 95.80/95.96 cnf(c283,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c105, c102])).
% 95.80/95.96 cnf(c285,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002)))|relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c283, c24])).
% 95.80/95.96 cnf(c299,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c285, c49])).
% 95.80/95.96 cnf(c1215,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c299, c248])).
% 95.80/95.96 cnf(c1222,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~rel_str(skolem0001)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1215, c24])).
% 95.80/95.96 cnf(c1225,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1222, c19])).
% 95.80/95.96 cnf(c1241,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1225, c22])).
% 95.80/95.96 cnf(c1255,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c1241, c93])).
% 95.80/95.96 cnf(c1259,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1255, c102])).
% 95.80/95.96 cnf(c1266,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c1259, c24])).
% 95.80/95.96 cnf(c64,plain,~rel_str(X228)|~element(X230,the_carrier(X228))|~relstr_element_smaller(X228,X229,X230)|~related(X228,skolem0010(X228,X229,X230),X230)|skolem0011(X228,X229,X230)!=X230|ex_inf_of_relstr_set(X228,X229),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c25,negated_conjecture,ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(X107,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X107)|related(skolem0001,X107,skolem0004),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c60,plain,~rel_str(X194)|~element(X196,the_carrier(X194))|~relstr_element_smaller(X194,X195,X196)|relstr_element_smaller(X194,X195,skolem0010(X194,X195,X196))|skolem0011(X194,X195,X196)!=X196|ex_inf_of_relstr_set(X194,X195),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c18,negated_conjecture,antisymmetric_relstr(skolem0001),inference(split_conjunct,[status(thm)],[c17])).
% 95.80/95.96 cnf(c61,plain,~rel_str(X203)|~element(X205,the_carrier(X203))|~relstr_element_smaller(X203,X204,X205)|~related(X203,skolem0010(X203,X204,X205),X205)|element(skolem0011(X203,X204,X205),the_carrier(X203))|ex_inf_of_relstr_set(X203,X204),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c53,plain,~rel_str(X128)|~element(X130,the_carrier(X128))|~relstr_element_smaller(X128,X129,X130)|element(skolem0010(X128,X129,X130),the_carrier(X128))|element(skolem0011(X128,X129,X130),the_carrier(X128))|ex_inf_of_relstr_set(X128,X129),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 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_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c53, c24])).
% 95.80/95.96 cnf(c616,plain,~rel_str(skolem0001)|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c170, c23])).
% 95.80/95.96 cnf(c625,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c616, c19])).
% 95.80/95.96 cnf(c57,plain,~rel_str(X162)|~element(X164,the_carrier(X162))|~relstr_element_smaller(X162,X163,X164)|relstr_element_smaller(X162,X163,skolem0010(X162,X163,X164))|element(skolem0011(X162,X163,X164),the_carrier(X162))|ex_inf_of_relstr_set(X162,X163),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.96 cnf(c201,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c57, c24])).
% 95.80/95.96 cnf(c790,plain,~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c201, c23])).
% 95.80/95.96 cnf(c792,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c790, c19])).
% 95.80/95.96 cnf(c807,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0010(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c792, c25])).
% 95.80/95.96 cnf(c2837,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0010(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c807, c625])).
% 95.80/95.97 cnf(c2863,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c2837, c61])).
% 95.80/95.97 cnf(c2895,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2863, c1266])).
% 95.80/95.97 cnf(c2896,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c2895, c1548])).
% 95.80/95.97 cnf(c2897,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2896, c19])).
% 95.80/95.97 cnf(c2899,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2897, c47])).
% 95.80/95.97 cnf(c2929,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2899, c19])).
% 95.80/95.97 cnf(c2901,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c2897, c48])).
% 95.80/95.97 cnf(c2933,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c2901, c19])).
% 95.80/95.97 cnf(c2947,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2933, c20])).
% 95.80/95.97 cnf(c3466,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c2947, c2929])).
% 95.80/95.97 cnf(c3468,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c3466, c2897])).
% 95.80/95.97 cnf(c2939,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c2933, c21])).
% 95.80/95.97 cnf(c3404,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c2939, c2929])).
% 95.80/95.97 cnf(c3406,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c3404, c2897])).
% 95.80/95.97 cnf(c3454,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c3406, c49])).
% 95.80/95.97 cnf(c13094,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c3454, c3468])).
% 95.80/95.97 cnf(c13097,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~rel_str(skolem0001)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c13094, c2897])).
% 95.80/95.97 cnf(c13102,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c13097, c19])).
% 95.80/95.97 cnf(c13120,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c13102, c22])).
% 95.80/95.97 cnf(c13128,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c13120, c2933])).
% 95.80/95.97 cnf(c13136,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|~ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c13128, c2929])).
% 95.80/95.97 cnf(c13138,plain,element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c13136, c2897])).
% 95.80/95.97 cnf(c62,plain,~rel_str(X214)|~element(X216,the_carrier(X214))|~relstr_element_smaller(X214,X215,X216)|~related(X214,skolem0010(X214,X215,X216),X216)|relstr_element_smaller(X214,X215,skolem0011(X214,X215,X216))|ex_inf_of_relstr_set(X214,X215),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c54,plain,~rel_str(X137)|~element(X139,the_carrier(X137))|~relstr_element_smaller(X137,X138,X139)|element(skolem0010(X137,X138,X139),the_carrier(X137))|relstr_element_smaller(X137,X138,skolem0011(X137,X138,X139))|ex_inf_of_relstr_set(X137,X138),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c179,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c54, c24])).
% 95.80/95.97 cnf(c669,plain,~rel_str(skolem0001)|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c179, c23])).
% 95.80/95.97 cnf(c671,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c669, c19])).
% 95.80/95.97 cnf(c58,plain,~rel_str(X172)|~element(X174,the_carrier(X172))|~relstr_element_smaller(X172,X173,X174)|relstr_element_smaller(X172,X173,skolem0010(X172,X173,X174))|relstr_element_smaller(X172,X173,skolem0011(X172,X173,X174))|ex_inf_of_relstr_set(X172,X173),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c211,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c58, c24])).
% 95.80/95.97 cnf(c879,plain,~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c211, c23])).
% 95.80/95.97 cnf(c881,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c879, c19])).
% 95.80/95.97 cnf(c896,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0010(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c881, c25])).
% 95.80/95.97 cnf(c3806,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0010(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c896, c671])).
% 95.80/95.97 cnf(c3844,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c3806, c62])).
% 95.80/95.97 cnf(c3905,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c3844, c1266])).
% 95.80/95.97 cnf(c3906,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c3905, c1548])).
% 95.80/95.97 cnf(c3907,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c3906, c19])).
% 95.80/95.97 cnf(c3922,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0011(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c3907, c25])).
% 95.80/95.97 cnf(c4075,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c3922, c2897])).
% 95.80/95.97 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)).
% 95.80/95.97 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])).
% 95.80/95.97 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])).])).
% 95.80/95.97 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])).
% 95.80/95.97 cnf(c59,plain,~rel_str(X181)|~element(X183,the_carrier(X181))|~relstr_element_smaller(X181,X182,X183)|relstr_element_smaller(X181,X182,skolem0010(X181,X182,X183))|~element(X184,the_carrier(X181))|~relstr_element_smaller(X181,X182,X184)|related(X181,X184,skolem0011(X181,X182,X183))|ex_inf_of_relstr_set(X181,X182),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c216,plain,~rel_str(X272)|~element(X270,the_carrier(X272))|~relstr_element_smaller(X272,X271,X270)|relstr_element_smaller(X272,X271,skolem0010(X272,X271,X270))|related(X272,X270,skolem0011(X272,X271,X270))|ex_inf_of_relstr_set(X272,X271),inference(factor,[status(thm)],[c59])).
% 95.80/95.97 cnf(c411,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c216, c24])).
% 95.80/95.97 cnf(c1817,plain,~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c411, c1548])).
% 95.80/95.97 cnf(c2110,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1817, c19])).
% 95.80/95.97 cnf(c2126,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~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)],[c2110, c11])).
% 95.80/95.97 cnf(c13417,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_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)],[c2126, c4075])).
% 95.80/95.97 cnf(c17210,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_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)],[c13417, c13138])).
% 95.80/95.97 cnf(c17211,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c17210, c1548])).
% 95.80/95.97 cnf(c17212,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c17211, c19])).
% 95.80/95.97 cnf(c17213,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c17212, c18])).
% 95.80/95.97 cnf(c17298,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c17213, c60])).
% 95.80/95.97 cnf(c18289,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c17298, c1266])).
% 95.80/95.97 cnf(c18290,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c18289, c1548])).
% 95.80/95.97 cnf(c18291,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0010(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c18290, c19])).
% 95.80/95.97 cnf(c18296,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0010(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c18291, c25])).
% 95.80/95.97 cnf(c56,plain,~rel_str(X154)|~element(X156,the_carrier(X154))|~relstr_element_smaller(X154,X155,X156)|element(skolem0010(X154,X155,X156),the_carrier(X154))|skolem0011(X154,X155,X156)!=X156|ex_inf_of_relstr_set(X154,X155),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c55,plain,~rel_str(X144)|~element(X146,the_carrier(X144))|~relstr_element_smaller(X144,X145,X146)|element(skolem0010(X144,X145,X146),the_carrier(X144))|~element(X147,the_carrier(X144))|~relstr_element_smaller(X144,X145,X147)|related(X144,X147,skolem0011(X144,X145,X146))|ex_inf_of_relstr_set(X144,X145),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c184,plain,~rel_str(X299)|~element(X298,the_carrier(X299))|~relstr_element_smaller(X299,X297,X298)|element(skolem0010(X299,X297,X298),the_carrier(X299))|related(X299,X298,skolem0011(X299,X297,X298))|ex_inf_of_relstr_set(X299,X297),inference(factor,[status(thm)],[c55])).
% 95.80/95.97 cnf(c435,plain,~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c184, c24])).
% 95.80/95.97 cnf(c2109,plain,~rel_str(skolem0001)|element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c435, c1548])).
% 95.80/95.97 cnf(c2136,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2109, c19])).
% 95.80/95.97 cnf(c2138,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~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)],[c2136, c11])).
% 95.80/95.97 cnf(c13454,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_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)],[c2138, c4075])).
% 95.80/95.97 cnf(c31839,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_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)],[c13454, c13138])).
% 95.80/95.97 cnf(c31840,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c31839, c1548])).
% 95.80/95.97 cnf(c31841,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c31840, c19])).
% 95.80/95.97 cnf(c31842,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c31841, c18])).
% 95.80/95.97 cnf(c31989,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c31842, c56])).
% 95.80/95.97 cnf(c34561,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c31989, c1266])).
% 95.80/95.97 cnf(c34563,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c34561, c1548])).
% 95.80/95.97 cnf(c34564,plain,element(skolem0010(skolem0001,skolem0002,skolem0004),the_carrier(skolem0001))|ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c34563, c19])).
% 95.80/95.97 cnf(c34580,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0010(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c34564, c18296])).
% 95.80/95.97 cnf(c34711,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004)|skolem0011(skolem0001,skolem0002,skolem0004)!=skolem0004,inference(resolution,[status(thm)],[c34580, c64])).
% 95.80/95.97 cnf(symmetry,axiom,X29!=X28|X28=X29,theory(equality)).
% 95.80/95.97 cnf(c4084,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4075, c47])).
% 95.80/95.97 cnf(c4191,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4084, c19])).
% 95.80/95.97 cnf(c4086,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c4075, c48])).
% 95.80/95.97 cnf(c4195,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c4086, c19])).
% 95.80/95.97 cnf(c4213,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4195, c20])).
% 95.80/95.97 cnf(c5685,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c4213, c4191])).
% 95.80/95.97 cnf(c5691,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c5685, c4075])).
% 95.80/95.97 cnf(c4199,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c4195, c21])).
% 95.80/95.97 cnf(c5645,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c4199, c4191])).
% 95.80/95.97 cnf(c5651,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c5645, c4075])).
% 95.80/95.97 cnf(c5665,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c5651, c49])).
% 95.80/95.97 cnf(c13787,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c5665, c5691])).
% 95.80/95.97 cnf(c13791,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~rel_str(skolem0001)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c13787, c4075])).
% 95.80/95.97 cnf(c13792,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c13791, c19])).
% 95.80/95.97 cnf(c13798,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c13792, c22])).
% 95.80/95.97 cnf(c13811,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c13798, c4195])).
% 95.80/95.97 cnf(c13814,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004)|~ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c13811, c4191])).
% 95.80/95.97 cnf(c13819,plain,related(skolem0001,skolem0011(skolem0001,skolem0002,skolem0004),skolem0004),inference(resolution,[status(thm)],[c13814, c4075])).
% 95.80/95.97 cnf(c13820,plain,~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)],[c13819, c11])).
% 95.80/95.97 cnf(c63,plain,~rel_str(X224)|~element(X226,the_carrier(X224))|~relstr_element_smaller(X224,X225,X226)|~related(X224,skolem0010(X224,X225,X226),X226)|~element(X227,the_carrier(X224))|~relstr_element_smaller(X224,X225,X227)|related(X224,X227,skolem0011(X224,X225,X226))|ex_inf_of_relstr_set(X224,X225),inference(split_conjunct,[status(thm)],[c46])).
% 95.80/95.97 cnf(c34715,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004)|~element(X7520,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,X7520)|related(skolem0001,X7520,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c34580, c63])).
% 95.80/95.97 cnf(c40601,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004)|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(factor,[status(thm)],[c34715])).
% 95.80/95.97 cnf(c40675,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c40601, c1266])).
% 95.80/95.97 cnf(c40676,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c40675, c1548])).
% 95.80/95.97 cnf(c40677,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0004,skolem0011(skolem0001,skolem0002,skolem0004)),inference(resolution,[status(thm)],[c40676, c19])).
% 95.80/95.97 cnf(c40751,plain,ex_inf_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)],[c40677, c13820])).
% 95.80/95.97 cnf(c42460,plain,ex_inf_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)],[c40751, c13138])).
% 95.80/95.97 cnf(c42461,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|~rel_str(skolem0001)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c42460, c1548])).
% 95.80/95.97 cnf(c42462,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~antisymmetric_relstr(skolem0001)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c42461, c19])).
% 95.80/95.97 cnf(c42463,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|skolem0004=skolem0011(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c42462, c18])).
% 95.80/95.97 cnf(c42536,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|skolem0011(skolem0001,skolem0002,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c42463, symmetry])).
% 95.80/95.97 cnf(c42681,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c42536, c34711])).
% 95.80/95.97 cnf(c43449,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001)|~element(skolem0004,the_carrier(skolem0001)),inference(resolution,[status(thm)],[c42681, c1266])).
% 95.80/95.97 cnf(c43450,plain,ex_inf_of_relstr_set(skolem0001,skolem0002)|~rel_str(skolem0001),inference(resolution,[status(thm)],[c43449, c1548])).
% 95.80/95.97 cnf(c43451,plain,ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c43450, c19])).
% 95.80/95.97 cnf(c43469,plain,~rel_str(skolem0001)|element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c43451, c47])).
% 95.80/95.97 cnf(c43558,plain,element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c43469, c19])).
% 95.80/95.97 cnf(c43453,plain,~rel_str(skolem0001)|relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c43451, c48])).
% 95.80/95.97 cnf(c43543,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c43453, c19])).
% 95.80/95.97 cnf(c43557,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c43543, c20])).
% 95.80/95.97 cnf(c44463,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c43557, c43558])).
% 95.80/95.97 cnf(c44464,plain,element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c44463, c43451])).
% 95.80/95.97 cnf(c43545,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c43543, c21])).
% 95.80/95.97 cnf(c44444,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c43545, c43558])).
% 95.80/95.97 cnf(c44445,plain,relstr_element_smaller(skolem0001,skolem0002,skolem0003(skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c44444, c43451])).
% 95.80/95.97 cnf(c44456,plain,~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0003(skolem0008(skolem0001,skolem0002)),the_carrier(skolem0001))|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c44445, c49])).
% 95.80/95.97 cnf(c45224,plain,~rel_str(skolem0001)|~ex_inf_of_relstr_set(skolem0001,skolem0002)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c44456, c44464])).
% 95.80/95.97 cnf(c45225,plain,~rel_str(skolem0001)|related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c45224, c43451])).
% 95.80/95.97 cnf(c45226,plain,related(skolem0001,skolem0003(skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c45225, c19])).
% 95.80/95.97 cnf(c45227,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001))|~relstr_element_smaller(skolem0001,skolem0002,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c45226, c22])).
% 95.80/95.97 cnf(c45230,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002)|~element(skolem0008(skolem0001,skolem0002),the_carrier(skolem0001)),inference(resolution,[status(thm)],[c45227, c43543])).
% 95.80/95.97 cnf(c45231,plain,~ex_inf_of_relstr_set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c45230, c43558])).
% 95.80/95.97 cnf(c45232,plain,$false,inference(resolution,[status(thm)],[c45231, c43451])).
% 95.80/95.97 % SZS output end CNFRefutation
% 95.80/95.97
% 95.80/95.97 % Initial clauses : 45
% 95.80/95.97 % Processed clauses : 5659
% 95.80/95.97 % Factors computed : 68
% 95.80/95.97 % Resolvents computed: 45100
% 95.80/95.97 % Tautologies deleted: 262
% 95.80/95.97 % Forward subsumed : 10093
% 95.80/95.97 % Backward subsumed : 5427
% 95.80/95.97 % -------- CPU Time ---------
% 95.80/95.97 % User time : 95.482 s
% 95.80/95.97 % System time : 0.145 s
% 95.80/95.97 % Total time : 95.627 s
%------------------------------------------------------------------------------