%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWB039+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:51:00 AM UTC 2026
% Result : Theorem 58.72s 13.75s
% Output : CNFRefutation 58.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB039+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.39 % Computer : n004.cluster.edu
% 0.09/5.39 % Model : x86_64 x86_64
% 0.09/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.39 % Memory : 8046.5625MB
% 0.09/5.39 % OS : Linux 6.8.0-71-generic
% 0.09/5.39 % CPULimit : 300
% 0.09/5.39 % WCLimit : 300
% 0.09/5.39 % DateTime : Sat Sep 26 11:54:29 UTC 2026
% 0.09/5.40 % CPUTime :
% 0.09/5.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.72/13.75 % SZS status Theorem for theBenchmark.p
% 58.72/13.75 % SZS output start CNFRefutation for theBenchmark.p
% 58.72/13.75 fof(premise_rdfbased_sem_bool_intersection_ext, axiom, ? [X0] : ? [X1] : ? [X2] : ((iext('uri$urdf$ufirst',X0,'uri$uex$uy') & (iext('uri$urdf$urest',X0,'uri$urdf$unil') & (iext('uri$uowl$uintersectionOf',X1,X2) & (iext('uri$urdf$ufirst',X2,'uri$uex$ux') & (iext('uri$urdf$urest',X2,X0) & iext('uri$uowl$uequivalentClass','uri$uex$uc',X1)))))))).
% 58.72/13.75 fof(owl_prop_equivalentclass_ext, axiom, ! [X0] : ! [X1] : ((iext('uri$uowl$uequivalentClass',X0,X1) => (ic(X0) & ic(X1))))).
% 58.72/13.75 fof(owl_bool_intersectionof_class_002, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((iext('uri$urdf$ufirst',X1,X2) & (iext('uri$urdf$urest',X1,X3) & (iext('uri$urdf$ufirst',X3,X4) & iext('uri$urdf$urest',X3,'uri$urdf$unil')))) => (iext('uri$uowl$uintersectionOf',X0,X1) <=> (ic(X0) & (ic(X2) & (ic(X4) & ! [X5] : ((icext(X0,X5) <=> (icext(X2,X5) & icext(X4,X5))))))))))).
% 58.72/13.75 fof(owl_eqdis_equivalentclass, axiom, ! [X0] : ! [X1] : ((iext('uri$uowl$uequivalentClass',X0,X1) <=> (ic(X0) & (ic(X1) & ! [X2] : ((icext(X0,X2) <=> icext(X1,X2)))))))).
% 58.72/13.75 fof(conclusion_rdfbased_sem_bool_intersection_ext, conjecture, ? [X0] : ? [X1] : ((iext('uri$urdf$ufirst',X1,'uri$uex$ux') & (iext('uri$urdf$urest',X1,X0) & (iext('uri$urdf$ufirst',X0,'uri$uex$uy') & (iext('uri$urdf$urest',X0,'uri$urdf$unil') & iext('uri$uowl$uintersectionOf','uri$uex$uc',X1))))))).
% 58.72/13.75 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ((iext('uri$urdf$ufirst',X1,'uri$uex$ux') & (iext('uri$urdf$urest',X1,X0) & (iext('uri$urdf$ufirst',X0,'uri$uex$uy') & (iext('uri$urdf$urest',X0,'uri$urdf$unil') & iext('uri$uowl$uintersectionOf','uri$uex$uc',X1)))))), inference(negate_conjecture, [status(cth)], [conclusion_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c0, plain, iext('uri$urdf$ufirst',sK0,'uri$uex$uy'), inference(clausification, [status(esa)], [premise_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c1, plain, iext('uri$urdf$urest',sK0,'uri$urdf$unil'), inference(clausification, [status(esa)], [premise_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c2, plain, iext('uri$uowl$uintersectionOf',sK1,sK2), inference(clausification, [status(esa)], [premise_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c3, plain, iext('uri$urdf$ufirst',sK2,'uri$uex$ux'), inference(clausification, [status(esa)], [premise_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c4, plain, iext('uri$urdf$urest',sK2,sK0), inference(clausification, [status(esa)], [premise_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c5, plain, iext('uri$uowl$uequivalentClass','uri$uex$uc',sK1), inference(clausification, [status(esa)], [premise_rdfbased_sem_bool_intersection_ext])).
% 58.72/13.75 cnf(c22, plain, ~iext('uri$uowl$uequivalentClass',X0,X1) | ic(X0), inference(clausification, [status(esa)], [owl_prop_equivalentclass_ext])).
% 58.72/13.75 cnf(c53, plain, ~iext('uri$urdf$ufirst',X0,X1) | ~iext('uri$urdf$urest',X2,'uri$urdf$unil') | ~iext('uri$urdf$ufirst',X2,X3) | ~iext('uri$uowl$uintersectionOf',X4,X0) | X5(X1,X3,X4) | ~iext('uri$urdf$urest',X0,X2), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c54, plain, ~iext('uri$urdf$ufirst',X0,X1) | ~iext('uri$urdf$urest',X2,'uri$urdf$unil') | ~iext('uri$urdf$ufirst',X2,X3) | iext('uri$uowl$uintersectionOf',X4,X0) | ~X5(X1,X3,X4) | ~iext('uri$urdf$urest',X0,X2), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c56, plain, ~X0(X1,X2,X3) | ic(X1), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c57, plain, ~X0(X1,X2,X3) | ic(X2), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c58, plain, ~X0(X1,X2,X3) | ~icext(X3,X4) | icext(X1,X4), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c59, plain, ~X0(X1,X2,X3) | ~icext(X3,X4) | icext(X2,X4), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c60, plain, ~X0(X1,X2,X3) | icext(X3,X4) | ~icext(X1,X4) | ~icext(X2,X4), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c62, plain, icext(X0,sK47(X1,X2,X0)) | ~ic(X2) | ~ic(X0) | X3(X1,X2,X0) | icext(X1,sK47(X1,X2,X0)) | ~ic(X1), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c63, plain, icext(X0,sK47(X1,X2,X0)) | ~ic(X2) | ~ic(X0) | ~ic(X1) | icext(X2,sK47(X1,X2,X0)) | X3(X1,X2,X0), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c64, plain, ~ic(X0) | ~ic(X1) | ~ic(X2) | ~icext(X0,sK47(X2,X0,X1)) | X3(X2,X0,X1) | ~icext(X1,sK47(X2,X0,X1)) | ~icext(X2,sK47(X2,X0,X1)), inference(clausification, [status(esa)], [owl_bool_intersectionof_class_002])).
% 58.72/13.75 cnf(c88, plain, ~iext('uri$uowl$uequivalentClass',X0,X1) | X2(X0,X1), inference(clausification, [status(esa)], [owl_eqdis_equivalentclass])).
% 58.72/13.75 cnf(c92, plain, ~X0(X1,X2) | ~icext(X1,X3) | icext(X2,X3), inference(clausification, [status(esa)], [owl_eqdis_equivalentclass])).
% 58.72/13.75 cnf(c93, plain, ~X0(X1,X2) | icext(X1,X3) | ~icext(X2,X3), inference(clausification, [status(esa)], [owl_eqdis_equivalentclass])).
% 58.72/13.75 cnf(c99, plain, ~iext('uri$urdf$ufirst',X0,'uri$uex$uy') | ~iext('uri$urdf$urest',X1,X0) | ~iext('uri$uowl$uintersectionOf','uri$uex$uc',X1) | ~iext('uri$urdf$urest',X0,'uri$urdf$unil') | ~iext('uri$urdf$ufirst',X1,'uri$uex$ux'), inference(clausification, [status(esa)], [negated_conjecture])).
% 58.72/13.75 cnf(d0, plain, ~iext('uri$urdf$ufirst',X0,X1) | ~iext('uri$urdf$ufirst',sK2,X2) | ~iext('uri$urdf$urest',X0,'uri$urdf$unil') | ~iext('uri$urdf$urest',sK2,X0) | 'Ts40'(X2,X1,sK1), inference(resolution, [status(thm)], [c53,c2])).
% 58.72/13.75 cnf(d1, plain, ~iext('uri$urdf$ufirst',sK0,X0) | ~iext('uri$urdf$ufirst',sK2,X1) | ~iext('uri$urdf$urest',sK0,'uri$urdf$unil') | 'Ts40'(X1,X0,sK1), inference(resolution, [status(thm)], [d0,c4])).
% 58.72/13.75 cnf(d2, plain, ~iext('uri$urdf$ufirst',sK0,X0) | ~iext('uri$urdf$ufirst',sK2,X1) | 'Ts40'(X1,X0,sK1), inference(resolution, [status(thm)], [c1,d1])).
% 58.72/13.75 cnf(d3, plain, ~iext('uri$urdf$ufirst',sK0,X0) | 'Ts40'('uri$uex$ux',X0,sK1), inference(resolution, [status(thm)], [d2,c3])).
% 58.72/13.75 cnf(d4, plain, 'Ts40'('uri$uex$ux','uri$uex$uy',sK1), inference(resolution, [status(thm)], [d3,c0])).
% 58.72/13.75 cnf(d5, plain, icext('uri$uex$uy',X0) | ~icext(sK1,X0), inference(resolution, [status(thm)], [d4,c59])).
% 58.72/13.75 cnf(d6, plain, 'Ts73'('uri$uex$uc',sK1), inference(resolution, [status(thm)], [c88,c5])).
% 58.72/13.75 cnf(d7, plain, icext(sK1,X0) | ~icext('uri$uex$uc',X0), inference(resolution, [status(thm)], [c92,d6])).
% 58.72/13.75 cnf(d8, plain, icext(sK1,X0) | ~icext('uri$uex$uy',X0) | ~icext('uri$uex$ux',X0), inference(resolution, [status(thm)], [d4,c60])).
% 58.72/13.75 cnf(d9, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux',X0,X1)) | icext(sK1,sK47('uri$uex$ux',X0,X1)) | icext(X1,sK47('uri$uex$ux',X0,X1)) | ~ic(X1) | ~ic('uri$uex$ux') | ~ic(X0) | 'Ts40'('uri$uex$ux',X0,X1), inference(resolution, [status(thm)], [d8,c62])).
% 58.72/13.75 cnf(d10, plain, ic('uri$uex$ux'), inference(resolution, [status(thm)], [d4,c56])).
% 58.72/13.75 cnf(d11, plain, icext(X0,sK47('uri$uex$ux',X1,X0)) | ~icext('uri$uex$uy',sK47('uri$uex$ux',X1,X0)) | icext(sK1,sK47('uri$uex$ux',X1,X0)) | ~ic(X0) | ~ic(X1) | 'Ts40'('uri$uex$ux',X1,X0), inference(resolution, [status(thm)], [d10,d9])).
% 58.72/13.75 cnf(d12, plain, icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | icext(sK1,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic('uri$uex$uy') | ~ic(X0) | 'Ts40'('uri$uex$ux','uri$uex$uy',X0) | icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic(X0) | ~ic('uri$uex$ux') | ~ic('uri$uex$uy') | 'Ts40'('uri$uex$ux','uri$uex$uy',X0), inference(resolution, [status(thm)], [d11,c63])).
% 58.72/13.75 cnf(d13, plain, icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | icext(sK1,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic(X0) | ~ic('uri$uex$uy') | 'Ts40'('uri$uex$ux','uri$uex$uy',X0), inference(resolution, [status(thm)], [d10,d12])).
% 58.72/13.75 cnf(d14, plain, ic('uri$uex$uy'), inference(resolution, [status(thm)], [d4,c57])).
% 58.72/13.75 cnf(d15, plain, icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | icext(sK1,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic(X0) | 'Ts40'('uri$uex$ux','uri$uex$uy',X0), inference(resolution, [status(thm)], [d14,d13])).
% 58.72/13.75 cnf(d16, plain, icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic(X0) | 'Ts40'('uri$uex$ux','uri$uex$uy',X0) | icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy',X0)), inference(resolution, [status(thm)], [d15,d5])).
% 58.72/13.75 cnf(d17, plain, icext('uri$uex$ux',X0) | ~icext(sK1,X0), inference(resolution, [status(thm)], [d4,c58])).
% 58.72/13.75 cnf(d18, plain, icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic(X0) | 'Ts40'('uri$uex$ux','uri$uex$uy',X0) | icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy',X0)), inference(resolution, [status(thm)], [d15,d17])).
% 58.72/13.75 cnf(d19, plain, icext('uri$uex$uc',X0) | ~icext(sK1,X0), inference(resolution, [status(thm)], [c93,d6])).
% 58.72/13.75 cnf(d20, plain, icext(X0,sK47('uri$uex$ux','uri$uex$uy',X0)) | ~ic(X0) | 'Ts40'('uri$uex$ux','uri$uex$uy',X0) | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy',X0)), inference(resolution, [status(thm)], [d15,d19])).
% 58.72/13.75 cnf(d21, plain, icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uy') | ~ic('uri$uex$ux') | ~ic('uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d20,c64])).
% 58.72/13.75 cnf(d22, plain, ic('uri$uex$uc'), inference(resolution, [status(thm)], [c22,c5])).
% 58.72/13.75 cnf(d23, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uy') | ~ic('uri$uex$ux') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d22,d21])).
% 58.72/13.75 cnf(d24, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uy') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d10,d23])).
% 58.72/13.75 cnf(d25, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d14,d24])).
% 58.72/13.75 cnf(d26, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d25,d18])).
% 58.72/13.75 cnf(d27, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d22,d26])).
% 58.72/13.75 cnf(d28, plain, icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d27,d16])).
% 58.72/13.75 cnf(d29, plain, icext('uri$uex$uc',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d22,d28])).
% 58.72/13.75 cnf(d30, plain, 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | icext(sK1,sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')), inference(resolution, [status(thm)], [d29,d7])).
% 58.72/13.75 cnf(d31, plain, 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')), inference(resolution, [status(thm)], [d30,d5])).
% 58.72/13.75 cnf(d32, plain, 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')), inference(resolution, [status(thm)], [d30,d17])).
% 58.72/13.75 cnf(d33, plain, 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uy') | ~ic('uri$uex$ux') | ~ic('uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d29,c64])).
% 58.72/13.75 cnf(d34, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uy') | ~ic('uri$uex$ux') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d22,d33])).
% 58.72/13.75 cnf(d35, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~ic('uri$uex$uy') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d10,d34])).
% 58.72/13.75 cnf(d36, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | ~icext('uri$uex$ux',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d14,d35])).
% 58.72/13.75 cnf(d37, plain, ~icext('uri$uex$uy',sK47('uri$uex$ux','uri$uex$uy','uri$uex$uc')) | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d36,d32])).
% 58.72/13.75 cnf(d38, plain, 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc') | 'Ts40'('uri$uex$ux','uri$uex$uy','uri$uex$uc'), inference(resolution, [status(thm)], [d37,d31])).
% 58.72/13.75 cnf(d39, plain, ~iext('uri$urdf$ufirst',X0,'uri$uex$uy') | ~iext('uri$urdf$ufirst',X1,'uri$uex$ux') | ~iext('uri$urdf$urest',X0,'uri$urdf$unil') | ~iext('uri$urdf$urest',X1,X0) | iext('uri$uowl$uintersectionOf','uri$uex$uc',X1), inference(resolution, [status(thm)], [d38,c54])).
% 58.72/13.75 cnf(d40, plain, ~iext('uri$urdf$ufirst',X0,'uri$uex$ux') | ~iext('uri$urdf$ufirst',sK0,'uri$uex$uy') | ~iext('uri$urdf$urest',X0,sK0) | iext('uri$uowl$uintersectionOf','uri$uex$uc',X0), inference(resolution, [status(thm)], [d39,c1])).
% 58.72/13.75 cnf(d41, plain, ~iext('uri$urdf$ufirst',X0,'uri$uex$ux') | ~iext('uri$urdf$urest',X0,sK0) | iext('uri$uowl$uintersectionOf','uri$uex$uc',X0), inference(resolution, [status(thm)], [c0,d40])).
% 58.72/13.75 cnf(d42, plain, ~iext('uri$urdf$ufirst',sK2,'uri$uex$ux') | iext('uri$uowl$uintersectionOf','uri$uex$uc',sK2), inference(resolution, [status(thm)], [d41,c4])).
% 58.72/13.75 cnf(d43, plain, iext('uri$uowl$uintersectionOf','uri$uex$uc',sK2), inference(resolution, [status(thm)], [c3,d42])).
% 58.72/13.75 cnf(d44, plain, ~iext('uri$urdf$ufirst',X0,'uri$uex$uy') | ~iext('uri$urdf$ufirst',sK2,'uri$uex$ux') | ~iext('uri$urdf$urest',X0,'uri$urdf$unil') | ~iext('uri$urdf$urest',sK2,X0), inference(resolution, [status(thm)], [d43,c99])).
% 58.72/13.75 cnf(d45, plain, ~iext('uri$urdf$ufirst',X0,'uri$uex$uy') | ~iext('uri$urdf$urest',X0,'uri$urdf$unil') | ~iext('uri$urdf$urest',sK2,X0), inference(resolution, [status(thm)], [c3,d44])).
% 58.72/13.75 cnf(d46, plain, ~iext('uri$urdf$ufirst',sK0,'uri$uex$uy') | ~iext('uri$urdf$urest',sK0,'uri$urdf$unil'), inference(resolution, [status(thm)], [d45,c4])).
% 58.72/13.75 cnf(d47, plain, ~iext('uri$urdf$urest',sK0,'uri$urdf$unil'), inference(resolution, [status(thm)], [c0,d46])).
% 58.72/13.75 cnf(d48, plain, $false, inference(resolution, [status(thm)], [c1,d47])).
% 58.72/13.75 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------