%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWB045+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:01 AM UTC 2026
% Result : Theorem 44.32s 7.38s
% Output : CNFRefutation 44.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB045+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 26 11:55:56 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.32/7.38 % SZS status Theorem for theBenchmark.p
% 44.32/7.38 % SZS output start CNFRefutation for theBenchmark.p
% 44.32/7.38 fof(premise_rdfbased_sem_char_functional_ext, axiom, ? [X0] : ? [X1] : ((iext('uri$urdfs$urange','uri$uex$up',X0) & (iext('uri$uex$up','uri$uex$ux','uri$uex$uy') & (iext('uri$urdf$ufirst',X1,'uri$uex$uy') & (iext('uri$urdf$urest',X1,'uri$urdf$unil') & iext('uri$uowl$uoneOf',X0,X1))))))).
% 44.32/7.38 fof(simple_iext_property, axiom, ! [X0] : ! [X1] : ! [X2] : ((iext(X1,X0,X2) => ip(X1)))).
% 44.32/7.38 fof(rdfs_cext_def, axiom, ! [X0] : ! [X1] : ((iext('uri$urdf$utype',X0,X1) <=> icext(X1,X0)))).
% 44.32/7.38 fof(rdfs_range_main, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((iext('uri$urdfs$urange',X0,X1) & iext(X0,X2,X3)) => icext(X1,X3)))).
% 44.32/7.38 fof(owl_enum_class_001, axiom, ! [X0] : ! [X1] : ! [X2] : (((iext('uri$urdf$ufirst',X1,X2) & iext('uri$urdf$urest',X1,'uri$urdf$unil')) => (iext('uri$uowl$uoneOf',X0,X1) <=> (ic(X0) & ! [X3] : ((icext(X0,X3) <=> X3 = X2))))))).
% 44.32/7.38 fof(owl_char_functional, axiom, ! [X0] : ((icext('uri$uowl$uFunctionalProperty',X0) <=> (ip(X0) & ! [X1] : ! [X2] : ! [X3] : (((iext(X0,X1,X2) & iext(X0,X1,X3)) => X2 = X3)))))).
% 44.32/7.38 fof(conclusion_rdfbased_sem_char_functional_ext, conjecture, iext('uri$urdf$utype','uri$uex$up','uri$uowl$uFunctionalProperty')).
% 44.32/7.38 fof(negated_conjecture, negated_conjecture, ~iext('uri$urdf$utype','uri$uex$up','uri$uowl$uFunctionalProperty'), inference(negate_conjecture, [status(cth)], [conclusion_rdfbased_sem_char_functional_ext])).
% 44.32/7.38 cnf(c0, plain, iext('uri$urdfs$urange','uri$uex$up',sK0), inference(clausification, [status(esa)], [premise_rdfbased_sem_char_functional_ext])).
% 44.32/7.38 cnf(c1, plain, iext('uri$uex$up','uri$uex$ux','uri$uex$uy'), inference(clausification, [status(esa)], [premise_rdfbased_sem_char_functional_ext])).
% 44.32/7.38 cnf(c2, plain, iext('uri$urdf$ufirst',sK1,'uri$uex$uy'), inference(clausification, [status(esa)], [premise_rdfbased_sem_char_functional_ext])).
% 44.32/7.38 cnf(c3, plain, iext('uri$urdf$urest',sK1,'uri$urdf$unil'), inference(clausification, [status(esa)], [premise_rdfbased_sem_char_functional_ext])).
% 44.32/7.38 cnf(c4, plain, iext('uri$uowl$uoneOf',sK0,sK1), inference(clausification, [status(esa)], [premise_rdfbased_sem_char_functional_ext])).
% 44.32/7.38 cnf(c5, plain, ~iext(X0,X1,X2) | ip(X0), inference(clausification, [status(esa)], [simple_iext_property])).
% 44.32/7.38 cnf(c16, plain, iext('uri$urdf$utype',X0,X1) | ~icext(X1,X0), inference(clausification, [status(esa)], [rdfs_cext_def])).
% 44.32/7.38 cnf(c33, plain, ~iext('uri$urdfs$urange',X0,X1) | ~iext(X0,X2,X3) | icext(X1,X3), inference(clausification, [status(esa)], [rdfs_range_main])).
% 44.32/7.38 cnf(c87, plain, ~iext('uri$urdf$ufirst',X0,X1) | ~iext('uri$urdf$urest',X0,'uri$urdf$unil') | ~iext('uri$uowl$uoneOf',X2,X0) | X3(X1,X2), inference(clausification, [status(esa)], [owl_enum_class_001])).
% 44.32/7.38 cnf(c90, plain, ~X0(X1,X2) | ~icext(X2,X3) | X3 = X1, inference(clausification, [status(esa)], [owl_enum_class_001])).
% 44.32/7.38 cnf(c148, plain, icext('uri$uowl$uFunctionalProperty',X0) | ~X1(X0), inference(clausification, [status(esa)], [owl_char_functional])).
% 44.32/7.38 cnf(c151, plain, X0(X1) | ~ip(X1) | iext(X1,sK127(X1),sK128(X1)), inference(clausification, [status(esa)], [owl_char_functional])).
% 44.32/7.38 cnf(c152, plain, X0(X1) | ~ip(X1) | iext(X1,sK127(X1),sK129(X1)), inference(clausification, [status(esa)], [owl_char_functional])).
% 44.32/7.38 cnf(c153, plain, X0(X1) | ~ip(X1) | sK128(X1) != sK129(X1), inference(clausification, [status(esa)], [owl_char_functional])).
% 44.32/7.38 cnf(c156, plain, ~iext('uri$urdf$utype','uri$uex$up','uri$uowl$uFunctionalProperty'), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.32/7.38 cnf(d0, plain, ~iext('uri$uex$up',X0,X1) | icext(sK0,X1), inference(resolution, [status(thm)], [c33,c0])).
% 44.32/7.38 cnf(d1, plain, icext(sK0,sK128('uri$uex$up')) | ~ip('uri$uex$up') | 'Ts122'('uri$uex$up'), inference(resolution, [status(thm)], [d0,c151])).
% 44.32/7.38 cnf(d2, plain, ip('uri$uex$up'), inference(resolution, [status(thm)], [c5,c1])).
% 44.32/7.38 cnf(d3, plain, icext(sK0,sK128('uri$uex$up')) | 'Ts122'('uri$uex$up'), inference(resolution, [status(thm)], [d2,d1])).
% 44.32/7.38 cnf(d4, plain, ~icext('uri$uowl$uFunctionalProperty','uri$uex$up'), inference(resolution, [status(thm)], [c16,c156])).
% 44.32/7.38 cnf(d5, plain, ~'Ts122'('uri$uex$up'), inference(resolution, [status(thm)], [c148,d4])).
% 44.32/7.38 cnf(d6, plain, icext(sK0,sK128('uri$uex$up')), inference(resolution, [status(thm)], [d5,d3])).
% 44.32/7.38 cnf(d7, plain, ~iext('uri$urdf$ufirst',sK1,X0) | ~iext('uri$urdf$urest',sK1,'uri$urdf$unil') | 'Ts64'(X0,sK0), inference(resolution, [status(thm)], [c87,c4])).
% 44.32/7.38 cnf(d8, plain, ~iext('uri$urdf$ufirst',sK1,X0) | 'Ts64'(X0,sK0), inference(resolution, [status(thm)], [c3,d7])).
% 44.32/7.38 cnf(d9, plain, 'Ts64'('uri$uex$uy',sK0), inference(resolution, [status(thm)], [d8,c2])).
% 44.32/7.38 cnf(d10, plain, X0 = 'uri$uex$uy' | ~icext(sK0,X0), inference(resolution, [status(thm)], [d9,c90])).
% 44.32/7.38 cnf(d11, plain, sK128('uri$uex$up') = 'uri$uex$uy', inference(resolution, [status(thm)], [d10,d6])).
% 44.32/7.38 cnf(d12, plain, icext(sK0,sK129('uri$uex$up')) | ~ip('uri$uex$up') | 'Ts122'('uri$uex$up'), inference(resolution, [status(thm)], [d0,c152])).
% 44.32/7.38 cnf(d13, plain, icext(sK0,sK129('uri$uex$up')) | 'Ts122'('uri$uex$up'), inference(resolution, [status(thm)], [d2,d12])).
% 44.32/7.38 cnf(d14, plain, icext(sK0,sK129('uri$uex$up')), inference(resolution, [status(thm)], [d5,d13])).
% 44.32/7.38 cnf(d15, plain, sK129('uri$uex$up') = 'uri$uex$uy', inference(resolution, [status(thm)], [d10,d14])).
% 44.32/7.38 cnf(d16, plain, sK128('uri$uex$up') != 'uri$uex$uy' | ~ip('uri$uex$up') | 'Ts122'('uri$uex$up'), inference(superposition, [status(thm)], [d15,c153])).
% 44.32/7.38 cnf(d17, plain, 'uri$uex$uy' != 'uri$uex$uy' | ~ip('uri$uex$up') | 'Ts122'('uri$uex$up'), inference(demodulation, [status(thm)], [d16,d11])).
% 44.32/7.38 cnf(d18, plain, 'uri$uex$uy' != 'uri$uex$uy' | 'Ts122'('uri$uex$up'), inference(resolution, [status(thm)], [d2,d17])).
% 44.32/7.38 cnf(d19, plain, 'uri$uex$uy' != 'uri$uex$uy', inference(resolution, [status(thm)], [d5,d18])).
% 44.32/7.38 cnf(d20, plain, $false, inference(equality_resolution, [status(thm)], [d19])).
% 44.32/7.38 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------