%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS140+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 07:45:14 AM UTC 2026
% Result : Theorem 11.82s 2.87s
% Output : CNFRefutation 11.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS140+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n003.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 19:42:39 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.82/2.87 % SZS status Theorem for theBenchmark.p
% 11.82/2.87 % SZS output start CNFRefutation for theBenchmark.p
% 11.82/2.87 fof(axiom_0, axiom, ! [X0] : ((cowlThing(X0) & ~cowlNothing(X0)))).
% 11.82/2.87 fof(axiom_1, axiom, ! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0)))).
% 11.82/2.87 fof(axiom_2, axiom, ! [X0] : ! [X1] : ((rsymProp(X0,X1) => (X1 = ia | X1 = ib)))).
% 11.82/2.87 fof(axiom_3, axiom, ! [X0] : ! [X1] : ((rsymProp(X0,X1) => rsymProp(X1,X0)))).
% 11.82/2.87 fof(axiom_5, axiom, rsymProp(ia,ia)).
% 11.82/2.87 fof(axiom_7, axiom, rsymProp(ib,ib)).
% 11.82/2.87 fof(the_axiom, conjecture, (! [X0] : ((cowlThing(X0) & ~cowlNothing(X0))) & (! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0))) & (! [X0] : ! [X1] : ! [X2] : (((rsymProp(X0,X1) & rsymProp(X1,X2)) => rsymProp(X0,X2))) & ? [X0] : ((rsymProp(ia,X0) & cowlThing(X0))))))).
% 11.82/2.87 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ((cowlThing(X0) & ~cowlNothing(X0))) & (! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0))) & (! [X0] : ! [X1] : ! [X2] : (((rsymProp(X0,X1) & rsymProp(X1,X2)) => rsymProp(X0,X2))) & ? [X0] : ((rsymProp(ia,X0) & cowlThing(X0))))))), inference(negate_conjecture, [status(cth)], [the_axiom])).
% 11.82/2.87 cnf(c6, plain, cowlThing(X0), inference(clausification, [status(esa)], [axiom_0])).
% 11.82/2.87 cnf(c7, plain, ~cowlNothing(X0), inference(clausification, [status(esa)], [axiom_0])).
% 11.82/2.87 cnf(c8, plain, ~'xsd$ustring'(X0) | ~'xsd$uinteger'(X0), inference(clausification, [status(esa)], [axiom_1])).
% 11.82/2.87 cnf(c9, plain, 'xsd$ustring'(X0) | 'xsd$uinteger'(X0), inference(clausification, [status(esa)], [axiom_1])).
% 11.82/2.87 cnf(c10, plain, ~rsymProp(X0,X1) | X1 = ia | X1 = ib, inference(clausification, [status(esa)], [axiom_2])).
% 11.82/2.87 cnf(c11, plain, ~rsymProp(X0,X1) | rsymProp(X1,X0), inference(clausification, [status(esa)], [axiom_3])).
% 11.82/2.87 cnf(c13, plain, rsymProp(ia,ia), inference(clausification, [status(esa)], [axiom_5])).
% 11.82/2.87 cnf(c15, plain, rsymProp(ib,ib), inference(clausification, [status(esa)], [axiom_7])).
% 11.82/2.87 cnf(c17, plain, ~cowlThing(sK21) | 'xsd$ustring'(sK22) | ~'xsd$uinteger'(sK22) | ~X0 | cowlNothing(sK21), inference(clausification, [status(esa)], [negated_conjecture])).
% 11.82/2.87 cnf(c18, plain, 'xsd$uinteger'(sK22) | ~cowlThing(sK21) | ~X0 | ~'xsd$ustring'(sK22) | cowlNothing(sK21), inference(clausification, [status(esa)], [negated_conjecture])).
% 11.82/2.87 cnf(c20, plain, X0 | rsymProp(sK23,sK24) | ~rsymProp(ia,X1) | ~cowlThing(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 11.82/2.87 cnf(c21, plain, X0 | rsymProp(sK24,sK25) | ~rsymProp(ia,X1) | ~cowlThing(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 11.82/2.87 cnf(c22, plain, X0 | ~rsymProp(sK23,sK25) | ~rsymProp(ia,X1) | ~cowlThing(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 11.82/2.87 cnf(d0, plain, ~rsymProp(ia,X0) | ~rsymProp(sK23,sK25) | 'Ts20', inference(resolution, [status(thm)], [c6,c22])).
% 11.82/2.87 cnf(d1, plain, cowlNothing(sK21) | 'xsd$uinteger'(sK22) | ~'xsd$ustring'(sK22) | ~'Ts20', inference(resolution, [status(thm)], [c6,c18])).
% 11.82/2.87 cnf(d2, plain, 'xsd$uinteger'(sK22) | ~'xsd$ustring'(sK22) | ~'Ts20', inference(resolution, [status(thm)], [c7,d1])).
% 11.82/2.87 cnf(d3, plain, 'xsd$uinteger'(sK22) | ~'Ts20' | 'xsd$uinteger'(sK22), inference(resolution, [status(thm)], [d2,c9])).
% 11.82/2.87 cnf(d4, plain, cowlNothing(sK21) | ~'xsd$uinteger'(sK22) | 'xsd$ustring'(sK22) | ~'Ts20', inference(resolution, [status(thm)], [c6,c17])).
% 11.82/2.87 cnf(d5, plain, ~'xsd$uinteger'(sK22) | 'xsd$ustring'(sK22) | ~'Ts20', inference(resolution, [status(thm)], [c7,d4])).
% 11.82/2.87 cnf(d6, plain, ~'Ts20' | 'xsd$ustring'(sK22) | ~'Ts20', inference(resolution, [status(thm)], [d3,d5])).
% 11.82/2.87 cnf(d7, plain, ~'Ts20' | ~'xsd$uinteger'(sK22), inference(resolution, [status(thm)], [d6,c8])).
% 11.82/2.87 cnf(d8, plain, ~'Ts20' | ~'Ts20', inference(resolution, [status(thm)], [d7,d3])).
% 11.82/2.87 cnf(d9, plain, ~rsymProp(ia,X0) | ~rsymProp(sK23,sK25), inference(resolution, [status(thm)], [d8,d0])).
% 11.82/2.87 cnf(d10, plain, ~rsymProp(ia,X0) | rsymProp(sK23,sK24) | 'Ts20', inference(resolution, [status(thm)], [c6,c20])).
% 11.82/2.87 cnf(d11, plain, ~rsymProp(ia,X0) | rsymProp(sK23,sK24), inference(resolution, [status(thm)], [d8,d10])).
% 11.82/2.87 cnf(d12, plain, rsymProp(sK23,sK24), inference(resolution, [status(thm)], [d11,c13])).
% 11.82/2.87 cnf(d13, plain, rsymProp(sK24,sK23), inference(resolution, [status(thm)], [d12,c11])).
% 11.82/2.87 cnf(d14, plain, sK23 = ib | sK23 = ia, inference(resolution, [status(thm)], [d13,c10])).
% 11.82/2.87 cnf(d15, plain, ~rsymProp(ib,sK25) | ~rsymProp(ia,X0) | sK23 = ia, inference(superposition, [status(thm)], [d14,d9])).
% 11.82/2.87 cnf(d16, plain, sK23 = ia | ~rsymProp(ib,sK25), inference(resolution, [status(thm)], [d15,c13])).
% 11.82/2.87 cnf(d17, plain, ~rsymProp(ia,X0) | rsymProp(sK24,sK25) | 'Ts20', inference(resolution, [status(thm)], [c6,c21])).
% 11.82/2.87 cnf(d18, plain, ~rsymProp(ia,X0) | rsymProp(sK24,sK25), inference(resolution, [status(thm)], [d8,d17])).
% 11.82/2.87 cnf(d19, plain, rsymProp(sK24,sK25), inference(resolution, [status(thm)], [d18,c13])).
% 11.82/2.87 cnf(d20, plain, sK25 = ib | sK25 = ia, inference(resolution, [status(thm)], [d19,c10])).
% 11.82/2.87 cnf(d21, plain, ~rsymProp(sK23,ib) | ~rsymProp(ia,X0) | sK25 = ia, inference(superposition, [status(thm)], [d20,d9])).
% 11.82/2.87 cnf(d22, plain, ~rsymProp(ib,ib) | sK25 = ia | ~rsymProp(ia,X0) | sK23 = ia, inference(superposition, [status(thm)], [d14,d21])).
% 11.82/2.87 cnf(d23, plain, sK23 = ia | sK25 = ia | ~rsymProp(ia,X0), inference(resolution, [status(thm)], [c15,d22])).
% 11.82/2.87 cnf(d24, plain, sK23 = ia | sK25 = ia, inference(resolution, [status(thm)], [d23,c13])).
% 11.82/2.87 cnf(d25, plain, ~rsymProp(ib,ia) | sK23 = ia | sK23 = ia, inference(superposition, [status(thm)], [d24,d16])).
% 11.82/2.87 cnf(d26, plain, rsymProp(ib,sK24) | sK23 = ia, inference(superposition, [status(thm)], [d14,d12])).
% 11.82/2.87 cnf(d27, plain, sK24 = ib | sK24 = ia, inference(resolution, [status(thm)], [d12,c10])).
% 11.82/2.87 cnf(d28, plain, rsymProp(ib,sK25) | sK24 = ia, inference(superposition, [status(thm)], [d27,d19])).
% 11.82/2.87 cnf(d29, plain, sK23 = ia | sK24 = ia, inference(resolution, [status(thm)], [d16,d28])).
% 11.82/2.87 cnf(d30, plain, rsymProp(ib,ia) | sK23 = ia | sK23 = ia, inference(superposition, [status(thm)], [d29,d26])).
% 11.82/2.87 cnf(d31, plain, sK23 = ia | sK23 = ia, inference(resolution, [status(thm)], [d30,d25])).
% 11.82/2.87 cnf(d32, plain, ~rsymProp(ia,X0) | ~rsymProp(ia,sK25), inference(demodulation, [status(thm)], [d9,d31])).
% 11.82/2.87 cnf(d33, plain, rsymProp(sK25,sK24), inference(resolution, [status(thm)], [d19,c11])).
% 11.82/2.87 cnf(d34, plain, rsymProp(sK25,ib) | sK24 = ia, inference(superposition, [status(thm)], [d27,d33])).
% 11.82/2.87 cnf(d35, plain, rsymProp(sK23,ib) | sK24 = ia, inference(superposition, [status(thm)], [d27,d12])).
% 11.82/2.87 cnf(d36, plain, sK24 = ia | sK25 = ia | ~rsymProp(ia,X0), inference(resolution, [status(thm)], [d35,d21])).
% 11.82/2.87 cnf(d37, plain, sK24 = ia | sK25 = ia, inference(resolution, [status(thm)], [d36,c13])).
% 11.82/2.87 cnf(d38, plain, rsymProp(ia,ib) | sK24 = ia | sK24 = ia, inference(superposition, [status(thm)], [d37,d34])).
% 11.82/2.87 cnf(d39, plain, ~rsymProp(sK23,ia) | ~rsymProp(ia,X0) | sK24 = ia, inference(superposition, [status(thm)], [d37,d9])).
% 11.82/2.87 cnf(d40, plain, sK24 = ia | ~rsymProp(ia,X0) | ~rsymProp(ia,ia), inference(demodulation, [status(thm)], [d39,d31])).
% 11.82/2.87 cnf(d41, plain, sK24 = ia | ~rsymProp(ia,X0), inference(resolution, [status(thm)], [c13,d40])).
% 11.82/2.87 cnf(d42, plain, sK24 = ia | sK24 = ia, inference(resolution, [status(thm)], [d41,d38])).
% 11.82/2.87 cnf(d43, plain, rsymProp(ia,sK25), inference(demodulation, [status(thm)], [d19,d42])).
% 11.82/2.87 cnf(d44, plain, ~rsymProp(ia,X0), inference(resolution, [status(thm)], [d43,d32])).
% 11.82/2.87 cnf(d45, plain, $false, inference(resolution, [status(thm)], [d44,c13])).
% 11.82/2.87 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------