%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU340+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:41:43 AM UTC 2026
% Result : Theorem 16.69s 2.89s
% Output : CNFRefutation 16.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU340+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 09:10:33 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.69/2.89 % SZS status Theorem for theBenchmark.p
% 16.69/2.89 % SZS output start CNFRefutation for theBenchmark.p
% 16.69/2.89 fof(cc1_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : ((element(X2,powerset('cartesian$uproduct2'(X0,X1))) => relation(X2)))).
% 16.69/2.89 fof(d5_orders_2, axiom, ! [X0] : (('rel$ustr'(X0) => ('transitive$urelstr'(X0) <=> 'is$utransitive$uin'('the$uInternalRel'(X0),'the$ucarrier'(X0)))))).
% 16.69/2.89 fof(d8_relat_2, axiom, ! [X0] : ((relation(X0) => ! [X1] : (('is$utransitive$uin'(X0,X1) <=> ! [X2] : ! [X3] : ! [X4] : (((in(X2,X1) & (in(X3,X1) & (in(X4,X1) & (in('ordered$upair'(X2,X3),X0) & in('ordered$upair'(X3,X4),X0))))) => in('ordered$upair'(X2,X4),X0)))))))).
% 16.69/2.89 fof(d9_orders_2, axiom, ! [X0] : (('rel$ustr'(X0) => ! [X1] : ((element(X1,'the$ucarrier'(X0)) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => (related(X0,X1,X2) <=> in('ordered$upair'(X1,X2),'the$uInternalRel'(X0)))))))))).
% 16.69/2.89 fof(dt_m2_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('relation$uof2$uas$usubset'(X2,X0,X1) => element(X2,powerset('cartesian$uproduct2'(X0,X1)))))).
% 16.69/2.89 fof(dt_u1_orders_2, axiom, ! [X0] : (('rel$ustr'(X0) => 'relation$uof2$uas$usubset'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0))))).
% 16.69/2.89 fof(existence_m1_subset_1, axiom, ! [X0] : ? [X1] : element(X1,X0)).
% 16.69/2.89 fof(fc1_xboole_0, axiom, empty('empty$uset')).
% 16.69/2.89 fof(rc2_subset_1, axiom, ! [X0] : ? [X1] : ((element(X1,powerset(X0)) & empty(X1)))).
% 16.69/2.89 fof(t106_zfmisc_1, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((in('ordered$upair'(X0,X1),'cartesian$uproduct2'(X2,X3)) <=> (in(X0,X2) & in(X1,X3))))).
% 16.69/2.89 fof(t2_subset, axiom, ! [X0] : ! [X1] : ((element(X0,X1) => (empty(X1) | in(X0,X1))))).
% 16.69/2.89 fof(t3_subset, axiom, ! [X0] : ! [X1] : ((element(X0,powerset(X1)) <=> subset(X0,X1)))).
% 16.69/2.89 fof(t4_subset, axiom, ! [X0] : ! [X1] : ! [X2] : (((in(X0,X1) & element(X1,powerset(X2))) => element(X0,X2)))).
% 16.69/2.89 fof(t5_subset, axiom, ! [X0] : ! [X1] : ! [X2] : ~((in(X0,X1) & (element(X1,powerset(X2)) & empty(X2))))).
% 16.69/2.89 fof(t6_boole, axiom, ! [X0] : ((empty(X0) => X0 = 'empty$uset'))).
% 16.69/2.89 fof(t7_boole, axiom, ! [X0] : ! [X1] : ~((in(X0,X1) & empty(X1)))).
% 16.69/2.89 fof(t26_orders_2, conjecture, ! [X0] : ((('transitive$urelstr'(X0) & 'rel$ustr'(X0)) => ! [X1] : ((element(X1,'the$ucarrier'(X0)) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => ! [X3] : ((element(X3,'the$ucarrier'(X0)) => ((related(X0,X1,X2) & related(X0,X2,X3)) => related(X0,X1,X3))))))))))).
% 16.69/2.89 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((('transitive$urelstr'(X0) & 'rel$ustr'(X0)) => ! [X1] : ((element(X1,'the$ucarrier'(X0)) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => ! [X3] : ((element(X3,'the$ucarrier'(X0)) => ((related(X0,X1,X2) & related(X0,X2,X3)) => related(X0,X1,X3)))))))))), inference(negate_conjecture, [status(cth)], [t26_orders_2])).
% 16.69/2.89 cnf(c1, plain, ~element(X0,powerset('cartesian$uproduct2'(X1,X2))) | relation(X0), inference(clausification, [status(esa)], [cc1_relset_1])).
% 16.69/2.89 cnf(c3, plain, ~'rel$ustr'(X0) | ~'transitive$urelstr'(X0) | 'is$utransitive$uin'('the$uInternalRel'(X0),'the$ucarrier'(X0)), inference(clausification, [status(esa)], [d5_orders_2])).
% 16.69/2.89 cnf(c6, plain, ~relation(X0) | ~'is$utransitive$uin'(X0,X1) | X2(X0,X1), inference(clausification, [status(esa)], [d8_relat_2])).
% 16.69/2.89 cnf(c8, plain, in('ordered$upair'(X0,X1),X2) | ~in(X1,X3) | ~in(X0,X3) | ~in(X4,X3) | ~in('ordered$upair'(X4,X1),X2) | ~X5(X2,X3) | ~in('ordered$upair'(X0,X4),X2), inference(clausification, [status(esa)], [d8_relat_2])).
% 16.69/2.89 cnf(c15, plain, ~element(X0,'the$ucarrier'(X1)) | ~related(X1,X2,X0) | ~'rel$ustr'(X1) | ~element(X2,'the$ucarrier'(X1)) | in('ordered$upair'(X2,X0),'the$uInternalRel'(X1)), inference(clausification, [status(esa)], [d9_orders_2])).
% 16.69/2.89 cnf(c16, plain, ~element(X0,'the$ucarrier'(X1)) | ~'rel$ustr'(X1) | ~in('ordered$upair'(X2,X0),'the$uInternalRel'(X1)) | related(X1,X2,X0) | ~element(X2,'the$ucarrier'(X1)), inference(clausification, [status(esa)], [d9_orders_2])).
% 16.69/2.89 cnf(c18, plain, ~'relation$uof2$uas$usubset'(X0,X1,X2) | element(X0,powerset('cartesian$uproduct2'(X1,X2))), inference(clausification, [status(esa)], [dt_m2_relset_1])).
% 16.69/2.89 cnf(c19, plain, ~'rel$ustr'(X0) | 'relation$uof2$uas$usubset'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0)), inference(clausification, [status(esa)], [dt_u1_orders_2])).
% 16.69/2.89 cnf(c23, plain, element(sK33(X0),X0), inference(clausification, [status(esa)], [existence_m1_subset_1])).
% 16.69/2.89 cnf(c26, plain, empty('empty$uset'), inference(clausification, [status(esa)], [fc1_xboole_0])).
% 16.69/2.89 cnf(c33, plain, element(sK47(X0),powerset(X0)), inference(clausification, [status(esa)], [rc2_subset_1])).
% 16.69/2.89 cnf(c34, plain, empty(sK47(X0)), inference(clausification, [status(esa)], [rc2_subset_1])).
% 16.69/2.89 cnf(c40, plain, ~in('ordered$upair'(X0,X1),'cartesian$uproduct2'(X2,X3)) | in(X1,X3), inference(clausification, [status(esa)], [t106_zfmisc_1])).
% 16.69/2.89 cnf(c43, plain, ~element(X0,X1) | empty(X1) | in(X0,X1), inference(clausification, [status(esa)], [t2_subset])).
% 16.69/2.89 cnf(c44, plain, ~element(X0,powerset(X1)) | subset(X0,X1), inference(clausification, [status(esa)], [t3_subset])).
% 16.69/2.89 cnf(c45, plain, element(X0,powerset(X1)) | ~subset(X0,X1), inference(clausification, [status(esa)], [t3_subset])).
% 16.69/2.89 cnf(c46, plain, ~in(X0,X1) | ~element(X1,powerset(X2)) | element(X0,X2), inference(clausification, [status(esa)], [t4_subset])).
% 16.69/2.89 cnf(c47, plain, ~in(X0,X1) | ~element(X1,powerset(X2)) | ~empty(X2), inference(clausification, [status(esa)], [t5_subset])).
% 16.69/2.89 cnf(c48, plain, ~empty(X0) | X0 = 'empty$uset', inference(clausification, [status(esa)], [t6_boole])).
% 16.69/2.89 cnf(c49, plain, ~in(X0,X1) | ~empty(X1), inference(clausification, [status(esa)], [t7_boole])).
% 16.69/2.89 cnf(c51, plain, 'transitive$urelstr'(sK75), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c52, plain, 'rel$ustr'(sK75), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c53, plain, element(sK76,'the$ucarrier'(sK75)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c54, plain, element(sK77,'the$ucarrier'(sK75)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c55, plain, element(sK78,'the$ucarrier'(sK75)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c56, plain, related(sK75,sK76,sK77), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c57, plain, related(sK75,sK77,sK78), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(c58, plain, ~related(sK75,sK76,sK78), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.69/2.89 cnf(d0, plain, in(sK33(X0),X0) | empty(X0), inference(resolution, [status(thm)], [c43,c23])).
% 16.69/2.89 cnf(d1, plain, ~in(X0,X1) | ~empty(X2) | ~subset(X1,X2), inference(resolution, [status(thm)], [c47,c45])).
% 16.69/2.89 cnf(d2, plain, ~'relation$uof2$uas$usubset'(X0,X1,X2) | relation(X0), inference(resolution, [status(thm)], [c18,c1])).
% 16.69/2.89 cnf(d3, plain, relation('the$uInternalRel'(X0)) | ~'rel$ustr'(X0), inference(resolution, [status(thm)], [d2,c19])).
% 16.69/2.89 cnf(d4, plain, in(sK76,'the$ucarrier'(sK75)) | empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [c43,c53])).
% 16.69/2.89 cnf(d5, plain, in(sK77,'the$ucarrier'(sK75)) | empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [c43,c54])).
% 16.69/2.89 cnf(d6, plain, in(sK78,'the$ucarrier'(sK75)) | empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [c43,c55])).
% 16.69/2.89 cnf(d7, plain, ~relation('the$uInternalRel'(X0)) | 'Ts10'('the$uInternalRel'(X0),'the$ucarrier'(X0)) | ~'transitive$urelstr'(X0) | ~'rel$ustr'(X0), inference(resolution, [status(thm)], [c6,c3])).
% 16.69/2.89 cnf(d8, plain, ~element(X0,'the$ucarrier'(X1)) | ~element(X2,'the$ucarrier'(X1)) | ~'rel$ustr'(X1) | ~related(X1,X2,X0) | ~in(X0,X3) | ~in(X4,X3) | ~in(X2,X3) | ~in('ordered$upair'(X0,X4),'the$uInternalRel'(X1)) | in('ordered$upair'(X2,X4),'the$uInternalRel'(X1)) | ~'Ts10'('the$uInternalRel'(X1),X3), inference(resolution, [status(thm)], [c15,c8])).
% 16.69/2.89 cnf(d9, plain, ~in(X0,X1) | ~in(X2,X1) | ~in(X3,X1) | in('ordered$upair'(X2,X0),'the$uInternalRel'(X4)) | ~element(X2,'the$ucarrier'(X4)) | ~element(X3,'the$ucarrier'(X4)) | ~'rel$ustr'(X4) | ~'Ts10'('the$uInternalRel'(X4),X1) | ~related(X4,X2,X3) | ~element(X0,'the$ucarrier'(X4)) | ~element(X3,'the$ucarrier'(X4)) | ~'rel$ustr'(X4) | ~related(X4,X3,X0), inference(resolution, [status(thm)], [d8,c15])).
% 16.69/2.89 cnf(d10, plain, ~in(sK77,X0) | ~in(sK76,X0) | ~in(X1,X0) | in('ordered$upair'(sK76,X1),'the$uInternalRel'(sK75)) | ~element(sK77,'the$ucarrier'(sK75)) | ~element(sK76,'the$ucarrier'(sK75)) | ~element(X1,'the$ucarrier'(sK75)) | ~'rel$ustr'(sK75) | ~'Ts10'('the$uInternalRel'(sK75),X0) | ~related(sK75,sK77,X1), inference(resolution, [status(thm)], [d9,c56])).
% 16.69/2.89 cnf(d11, plain, ~in(X0,X1) | in('ordered$upair'(sK76,X0),'the$uInternalRel'(sK75)) | ~in(sK76,X1) | ~in(sK77,X1) | ~element(X0,'the$ucarrier'(sK75)) | ~element(sK76,'the$ucarrier'(sK75)) | ~element(sK77,'the$ucarrier'(sK75)) | ~'Ts10'('the$uInternalRel'(sK75),X1) | ~related(sK75,sK77,X0), inference(resolution, [status(thm)], [c52,d10])).
% 16.69/2.89 cnf(d12, plain, ~in(X0,X1) | in('ordered$upair'(sK76,X0),'the$uInternalRel'(sK75)) | ~in(sK76,X1) | ~in(sK77,X1) | ~element(X0,'the$ucarrier'(sK75)) | ~element(sK77,'the$ucarrier'(sK75)) | ~'Ts10'('the$uInternalRel'(sK75),X1) | ~related(sK75,sK77,X0), inference(resolution, [status(thm)], [c53,d11])).
% 16.69/2.89 cnf(d13, plain, ~in(X0,X1) | in('ordered$upair'(sK76,X0),'the$uInternalRel'(sK75)) | ~in(sK76,X1) | ~in(sK77,X1) | ~element(X0,'the$ucarrier'(sK75)) | ~'Ts10'('the$uInternalRel'(sK75),X1) | ~related(sK75,sK77,X0), inference(resolution, [status(thm)], [c54,d12])).
% 16.69/2.89 cnf(d14, plain, ~in(sK78,X0) | in('ordered$upair'(sK76,sK78),'the$uInternalRel'(sK75)) | ~in(sK76,X0) | ~in(sK77,X0) | ~element(sK78,'the$ucarrier'(sK75)) | ~'Ts10'('the$uInternalRel'(sK75),X0), inference(resolution, [status(thm)], [d13,c57])).
% 16.69/2.89 cnf(d15, plain, in('ordered$upair'(sK76,sK78),'the$uInternalRel'(sK75)) | ~in(sK76,X0) | ~in(sK77,X0) | ~in(sK78,X0) | ~'Ts10'('the$uInternalRel'(sK75),X0), inference(resolution, [status(thm)], [c55,d14])).
% 16.69/2.89 cnf(d16, plain, in('ordered$upair'(sK76,sK78),'the$uInternalRel'(sK75)) | ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | ~'transitive$urelstr'(sK75) | ~'rel$ustr'(sK75), inference(resolution, [status(thm)], [d15,d7])).
% 16.69/2.89 cnf(d17, plain, in('ordered$upair'(sK76,sK78),'the$uInternalRel'(sK75)) | ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | ~'rel$ustr'(sK75), inference(resolution, [status(thm)], [c51,d16])).
% 16.69/2.89 cnf(d18, plain, in('ordered$upair'(sK76,sK78),'the$uInternalRel'(sK75)) | ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [c52,d17])).
% 16.69/2.89 cnf(d19, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | ~element(sK78,'the$ucarrier'(sK75)) | ~element(sK76,'the$ucarrier'(sK75)) | ~'rel$ustr'(sK75) | related(sK75,sK76,sK78), inference(resolution, [status(thm)], [d18,c16])).
% 16.69/2.89 cnf(d20, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~element(sK76,'the$ucarrier'(sK75)) | ~element(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | related(sK75,sK76,sK78), inference(resolution, [status(thm)], [c52,d19])).
% 16.69/2.89 cnf(d21, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~element(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | related(sK75,sK76,sK78), inference(resolution, [status(thm)], [c53,d20])).
% 16.69/2.89 cnf(d22, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | related(sK75,sK76,sK78), inference(resolution, [status(thm)], [c55,d21])).
% 16.69/2.89 cnf(d23, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~in(sK78,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [c58,d22])).
% 16.69/2.89 cnf(d24, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~in(sK77,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [d23,d6])).
% 16.69/2.89 cnf(d25, plain, ~in(sK76,'the$ucarrier'(sK75)) | ~relation('the$uInternalRel'(sK75)) | empty('the$ucarrier'(sK75)) | empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [d24,d5])).
% 16.69/2.89 cnf(d26, plain, ~relation('the$uInternalRel'(sK75)) | empty('the$ucarrier'(sK75)) | empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [d25,d4])).
% 16.69/2.89 cnf(d27, plain, empty('the$ucarrier'(sK75)) | ~'rel$ustr'(sK75), inference(resolution, [status(thm)], [d26,d3])).
% 16.69/2.89 cnf(d28, plain, empty('the$ucarrier'(sK75)), inference(resolution, [status(thm)], [c52,d27])).
% 16.69/2.89 cnf(d29, plain, 'the$ucarrier'(sK75) = 'empty$uset', inference(resolution, [status(thm)], [d28,c48])).
% 16.69/2.89 cnf(d30, plain, 'relation$uof2$uas$usubset'('the$uInternalRel'(sK75),'empty$uset','the$ucarrier'(sK75)) | ~'rel$ustr'(sK75), inference(superposition, [status(thm)], [d29,c19])).
% 16.69/2.89 cnf(d31, plain, ~'rel$ustr'(sK75) | 'relation$uof2$uas$usubset'('the$uInternalRel'(sK75),'empty$uset','empty$uset'), inference(demodulation, [status(thm)], [d30,d29])).
% 16.69/2.89 cnf(d32, plain, 'relation$uof2$uas$usubset'('the$uInternalRel'(sK75),'empty$uset','empty$uset'), inference(resolution, [status(thm)], [c52,d31])).
% 16.69/2.89 cnf(d33, plain, subset(X0,'cartesian$uproduct2'(X1,X2)) | ~'relation$uof2$uas$usubset'(X0,X1,X2), inference(resolution, [status(thm)], [c44,c18])).
% 16.69/2.89 cnf(d34, plain, sK47(X0) = 'empty$uset', inference(resolution, [status(thm)], [c48,c34])).
% 16.69/2.89 cnf(d35, plain, element('empty$uset',powerset(X0)), inference(demodulation, [status(thm)], [c33,d34])).
% 16.69/2.89 cnf(d36, plain, ~in(X0,'empty$uset') | ~empty(X1), inference(resolution, [status(thm)], [c47,d35])).
% 16.69/2.89 cnf(d37, plain, ~in(X0,X1) | element(X0,'cartesian$uproduct2'(X2,X3)) | ~'relation$uof2$uas$usubset'(X1,X2,X3), inference(resolution, [status(thm)], [c46,c18])).
% 16.69/2.89 cnf(d38, plain, ~in(X0,'the$uInternalRel'(sK75)) | element(X0,'cartesian$uproduct2'('empty$uset','empty$uset')), inference(resolution, [status(thm)], [d32,d37])).
% 16.69/2.89 cnf(d39, plain, ~in(X0,'the$uInternalRel'(sK75)) | in(X0,'cartesian$uproduct2'('empty$uset','empty$uset')) | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(resolution, [status(thm)], [d38,c43])).
% 16.69/2.89 cnf(d40, plain, ~in('ordered$upair'(X0,X1),'the$uInternalRel'(sK75)) | empty('cartesian$uproduct2'('empty$uset','empty$uset')) | in(X1,'empty$uset'), inference(resolution, [status(thm)], [d39,c40])).
% 16.69/2.89 cnf(d41, plain, in(X0,'empty$uset') | empty('cartesian$uproduct2'('empty$uset','empty$uset')) | ~element(X0,'the$ucarrier'(sK75)) | ~element(X1,'the$ucarrier'(sK75)) | ~'rel$ustr'(sK75) | ~related(sK75,X1,X0), inference(resolution, [status(thm)], [d40,c15])).
% 16.69/2.89 cnf(d42, plain, in(X0,'empty$uset') | ~element(X1,'empty$uset') | ~element(X0,'the$ucarrier'(sK75)) | ~'rel$ustr'(sK75) | ~related(sK75,X1,X0) | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(demodulation, [status(thm)], [d41,d29])).
% 16.69/2.89 cnf(d43, plain, in(X0,'empty$uset') | ~element(X1,'empty$uset') | ~element(X0,'empty$uset') | ~'rel$ustr'(sK75) | ~related(sK75,X1,X0) | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(demodulation, [status(thm)], [d42,d29])).
% 16.69/2.89 cnf(d44, plain, in(X0,'empty$uset') | ~element(X1,'empty$uset') | ~element(X0,'empty$uset') | ~related(sK75,X1,X0) | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(resolution, [status(thm)], [c52,d43])).
% 16.69/2.89 cnf(d45, plain, in(sK77,'empty$uset') | ~element(sK76,'empty$uset') | ~element(sK77,'empty$uset') | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(resolution, [status(thm)], [d44,c56])).
% 16.69/2.89 cnf(d46, plain, element(sK77,'empty$uset'), inference(demodulation, [status(thm)], [c54,d29])).
% 16.69/2.89 cnf(d47, plain, in(sK77,'empty$uset') | ~element(sK76,'empty$uset') | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(resolution, [status(thm)], [d46,d45])).
% 16.69/2.89 cnf(d48, plain, element(sK76,'empty$uset'), inference(demodulation, [status(thm)], [c53,d29])).
% 16.69/2.89 cnf(d49, plain, in(sK77,'empty$uset') | empty('cartesian$uproduct2'('empty$uset','empty$uset')), inference(resolution, [status(thm)], [d48,d47])).
% 16.69/2.89 cnf(d50, plain, in(sK77,'empty$uset') | 'cartesian$uproduct2'('empty$uset','empty$uset') = 'empty$uset', inference(resolution, [status(thm)], [d49,c48])).
% 16.69/2.89 cnf(d51, plain, 'cartesian$uproduct2'('empty$uset','empty$uset') = 'empty$uset' | ~empty(X0), inference(resolution, [status(thm)], [d50,d36])).
% 16.69/2.89 cnf(d52, plain, 'cartesian$uproduct2'('empty$uset','empty$uset') = 'empty$uset', inference(resolution, [status(thm)], [d51,c26])).
% 16.69/2.89 cnf(d53, plain, subset(X0,'empty$uset') | ~'relation$uof2$uas$usubset'(X0,'empty$uset','empty$uset'), inference(superposition, [status(thm)], [d52,d33])).
% 16.69/2.89 cnf(d54, plain, subset('the$uInternalRel'(sK75),'empty$uset'), inference(resolution, [status(thm)], [d53,d32])).
% 16.69/2.89 cnf(d55, plain, ~in(X0,'the$uInternalRel'(sK75)) | ~empty('empty$uset'), inference(resolution, [status(thm)], [d54,d1])).
% 16.69/2.89 cnf(d56, plain, ~in(X0,'the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [c26,d55])).
% 16.69/2.89 cnf(d57, plain, empty('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [d56,d0])).
% 16.69/2.89 cnf(d58, plain, ~empty('the$uInternalRel'(X0)) | ~element(X1,'the$ucarrier'(X0)) | ~element(X2,'the$ucarrier'(X0)) | ~'rel$ustr'(X0) | ~related(X0,X2,X1), inference(resolution, [status(thm)], [c49,c15])).
% 16.69/2.89 cnf(d59, plain, ~element(sK76,'the$ucarrier'(sK75)) | ~element(sK77,'the$ucarrier'(sK75)) | ~'rel$ustr'(sK75) | ~empty('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [d58,c56])).
% 16.69/2.89 cnf(d60, plain, ~element(sK76,'the$ucarrier'(sK75)) | ~element(sK77,'the$ucarrier'(sK75)) | ~empty('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [c52,d59])).
% 16.69/2.89 cnf(d61, plain, ~element(sK77,'the$ucarrier'(sK75)) | ~empty('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [c53,d60])).
% 16.69/2.89 cnf(d62, plain, ~empty('the$uInternalRel'(sK75)), inference(resolution, [status(thm)], [c54,d61])).
% 16.69/2.89 cnf(d63, plain, $false, inference(resolution, [status(thm)], [d62,d57])).
% 16.69/2.89 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------