%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS138+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 15.01s 8.77s
% Output : CNFRefutation 15.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS138+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n007.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Fri Sep 25 19:38:59 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.01/8.77 % SZS status Theorem for theBenchmark.p
% 15.01/8.77 % SZS output start CNFRefutation for theBenchmark.p
% 15.01/8.77 fof(axiom_0, axiom, ! [X0] : ((cowlThing(X0) & ~cowlNothing(X0)))).
% 15.01/8.77 fof(axiom_1, axiom, ! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0)))).
% 15.01/8.77 fof(axiom_2, axiom, ! [X0] : ((cA(X0) <=> (X0 = ib | X0 = ia)))).
% 15.01/8.77 fof(axiom_3, axiom, ! [X0] : ! [X1] : ! [X2] : (((requalityOnA(X1,X0) & requalityOnA(X2,X0)) => X1 = X2))).
% 15.01/8.77 fof(axiom_4, axiom, ! [X0] : ! [X1] : ((requalityOnA(X0,X1) => cA(X1)))).
% 15.01/8.77 fof(axiom_6, axiom, requalityOnA(ia,ia)).
% 15.01/8.77 fof(axiom_8, axiom, requalityOnA(ib,ib)).
% 15.01/8.77 fof(the_axiom, conjecture, (! [X0] : ((cowlThing(X0) & ~cowlNothing(X0))) & (! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0))) & (! [X0] : ! [X1] : ((requalityOnA(X0,X1) => (X0 = ia | (X0 = ib | X0 = ic)))) & (! [X0] : ! [X1] : ((requalityOnA(X0,X1) => requalityOnA(X1,X0))) & (cowlThing(ia) & (requalityOnA(ia,ia) & (cowlThing(ib) & cowlThing(ic))))))))).
% 15.01/8.77 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ((cowlThing(X0) & ~cowlNothing(X0))) & (! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0))) & (! [X0] : ! [X1] : ((requalityOnA(X0,X1) => (X0 = ia | (X0 = ib | X0 = ic)))) & (! [X0] : ! [X1] : ((requalityOnA(X0,X1) => requalityOnA(X1,X0))) & (cowlThing(ia) & (requalityOnA(ia,ia) & (cowlThing(ib) & cowlThing(ic))))))))), inference(negate_conjecture, [status(cth)], [the_axiom])).
% 15.01/8.77 cnf(c7, plain, cowlThing(X0), inference(clausification, [status(esa)], [axiom_0])).
% 15.01/8.77 cnf(c8, plain, ~cowlNothing(X0), inference(clausification, [status(esa)], [axiom_0])).
% 15.01/8.77 cnf(c9, plain, ~'xsd$ustring'(X0) | ~'xsd$uinteger'(X0), inference(clausification, [status(esa)], [axiom_1])).
% 15.01/8.77 cnf(c10, plain, 'xsd$ustring'(X0) | 'xsd$uinteger'(X0), inference(clausification, [status(esa)], [axiom_1])).
% 15.01/8.77 cnf(c11, plain, ~cA(X0) | X0 = ib | X0 = ia, inference(clausification, [status(esa)], [axiom_2])).
% 15.01/8.77 cnf(c14, plain, ~requalityOnA(X0,X1) | ~requalityOnA(X2,X1) | X0 = X2, inference(clausification, [status(esa)], [axiom_3])).
% 15.01/8.77 cnf(c15, plain, ~requalityOnA(X0,X1) | cA(X1), inference(clausification, [status(esa)], [axiom_4])).
% 15.01/8.77 cnf(c17, plain, requalityOnA(ia,ia), inference(clausification, [status(esa)], [axiom_6])).
% 15.01/8.77 cnf(c19, plain, requalityOnA(ib,ib), inference(clausification, [status(esa)], [axiom_8])).
% 15.01/8.77 cnf(c23, plain, ~cowlThing(ic) | ~requalityOnA(ia,ia) | ~'xsd$uinteger'(sK26) | ~cowlThing(sK25) | ~X0 | ~cowlThing(ib) | 'xsd$ustring'(sK26) | ~cowlThing(ia) | requalityOnA(sK27,sK28) | cowlNothing(sK25), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(c24, plain, ~cowlThing(ic) | ~'xsd$uinteger'(sK26) | ~cowlThing(sK25) | ~X0 | ~cowlThing(ib) | 'xsd$ustring'(sK26) | ~cowlThing(ia) | cowlNothing(sK25) | ~requalityOnA(ia,ia) | ~requalityOnA(sK28,sK27), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(c25, plain, ~cowlThing(ic) | ~requalityOnA(ia,ia) | ~cowlThing(sK25) | ~X0 | ~cowlThing(ib) | ~'xsd$ustring'(sK26) | 'xsd$uinteger'(sK26) | ~cowlThing(ia) | requalityOnA(sK27,sK28) | cowlNothing(sK25), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(c26, plain, ~cowlThing(ic) | ~cowlThing(sK25) | ~X0 | ~cowlThing(ib) | ~'xsd$ustring'(sK26) | 'xsd$uinteger'(sK26) | ~cowlThing(ia) | cowlNothing(sK25) | ~requalityOnA(ia,ia) | ~requalityOnA(sK28,sK27), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(c29, plain, X0 | requalityOnA(sK29,sK30), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(c30, plain, X0 | sK29 != ia, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(c31, plain, X0 | sK29 != ib, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.01/8.77 cnf(d0, plain, X0 = ia | ~requalityOnA(X0,ia), inference(resolution, [status(thm)], [c17,c14])).
% 15.01/8.77 cnf(d1, plain, cowlNothing(sK25) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | requalityOnA(sK27,sK28) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,c25])).
% 15.01/8.77 cnf(d2, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | requalityOnA(sK27,sK28) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c8,d1])).
% 15.01/8.77 cnf(d3, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | requalityOnA(sK27,sK28) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d2])).
% 15.01/8.77 cnf(d4, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | X0 = sK27 | ~requalityOnA(X0,sK28), inference(resolution, [status(thm)], [d3,c14])).
% 15.01/8.77 cnf(d5, plain, X0 = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(X0,sK28) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d4])).
% 15.01/8.77 cnf(d6, plain, cowlNothing(sK25) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | ~requalityOnA(sK28,sK27) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,c26])).
% 15.01/8.77 cnf(d7, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | ~requalityOnA(sK28,sK27) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c8,d6])).
% 15.01/8.77 cnf(d8, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(sK28,sK27) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d7])).
% 15.01/8.77 cnf(d9, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | cA(sK28), inference(resolution, [status(thm)], [d3,c15])).
% 15.01/8.77 cnf(d10, plain, cA(sK28) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d9])).
% 15.01/8.77 cnf(d11, plain, cA(sK28) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d10,c10])).
% 15.01/8.77 cnf(d12, plain, cA(sK28) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d11])).
% 15.01/8.77 cnf(d13, plain, cA(sK28) | 'xsd$uinteger'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d12,c7])).
% 15.01/8.77 cnf(d14, plain, 'xsd$uinteger'(sK26) | ~'Ts24' | sK28 = ib | sK28 = ia, inference(resolution, [status(thm)], [d13,c11])).
% 15.01/8.77 cnf(d15, plain, cowlNothing(sK25) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | requalityOnA(sK27,sK28) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,c23])).
% 15.01/8.77 cnf(d16, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | requalityOnA(sK27,sK28) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c8,d15])).
% 15.01/8.77 cnf(d17, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | requalityOnA(sK27,sK28) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d16])).
% 15.01/8.77 cnf(d18, plain, ~cowlThing(ic) | ~cowlThing(sK25) | requalityOnA(sK27,sK28) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d17])).
% 15.01/8.77 cnf(d19, plain, ~cowlThing(ic) | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | cA(sK28), inference(resolution, [status(thm)], [d18,c15])).
% 15.01/8.77 cnf(d20, plain, cA(sK28) | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d19])).
% 15.01/8.77 cnf(d21, plain, sK28 = ib | sK28 = ia | ~'Ts24' | cA(sK28) | ~cowlThing(sK25) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d14,d20])).
% 15.01/8.77 cnf(d22, plain, sK28 = ib | sK28 = ia | cA(sK28) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d21])).
% 15.01/8.77 cnf(d23, plain, sK28 = ib | sK28 = ia | 'xsd$ustring'(sK26) | ~'Ts24' | sK28 = ib | sK28 = ia, inference(resolution, [status(thm)], [d22,c11])).
% 15.01/8.77 cnf(d24, plain, sK28 = ib | sK28 = ia | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d23,c9])).
% 15.01/8.77 cnf(d25, plain, sK28 = ib | sK28 = ia | ~'Ts24' | sK28 = ib | sK28 = ia | ~'Ts24', inference(resolution, [status(thm)], [d24,d14])).
% 15.01/8.77 cnf(d26, plain, X0 = ib | ~requalityOnA(X0,ib), inference(resolution, [status(thm)], [c19,c14])).
% 15.01/8.77 cnf(d27, plain, cA(sK30) | 'Ts24', inference(resolution, [status(thm)], [c15,c29])).
% 15.01/8.77 cnf(d28, plain, 'Ts24' | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d27,c11])).
% 15.01/8.77 cnf(d29, plain, sK28 = ib | sK28 = ia | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d25,d28])).
% 15.01/8.77 cnf(d30, plain, requalityOnA(sK29,ib) | 'Ts24' | sK28 = ib | sK28 = ia | sK30 = ia, inference(superposition, [status(thm)], [d29,c29])).
% 15.01/8.77 cnf(d31, plain, sK28 = ib | sK28 = ia | sK30 = ia | 'Ts24' | sK29 = ib, inference(resolution, [status(thm)], [d30,d26])).
% 15.01/8.77 cnf(d32, plain, sK28 = ib | sK28 = ia | sK29 = ib | sK30 = ia | sK28 = ib | sK28 = ia, inference(resolution, [status(thm)], [d31,d25])).
% 15.01/8.77 cnf(d33, plain, requalityOnA(sK29,ia) | 'Ts24' | sK28 = ib | sK28 = ia | sK29 = ib, inference(superposition, [status(thm)], [d32,c29])).
% 15.01/8.77 cnf(d34, plain, sK28 = ib | sK28 = ia | sK29 = ib | 'Ts24' | sK29 = ia, inference(resolution, [status(thm)], [d33,d0])).
% 15.01/8.77 cnf(d35, plain, sK28 = ib | sK28 = ia | sK29 = ib | sK29 = ia | sK28 = ib | sK28 = ia, inference(resolution, [status(thm)], [d34,d25])).
% 15.01/8.77 cnf(d36, plain, ib != ib | 'Ts24' | sK28 = ib | sK28 = ia | sK29 = ia, inference(superposition, [status(thm)], [d35,c31])).
% 15.01/8.77 cnf(d37, plain, sK28 = ib | sK28 = ia | sK29 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d36])).
% 15.01/8.77 cnf(d38, plain, sK28 = ib | sK28 = ia | sK29 = ia | sK28 = ib | sK28 = ia, inference(resolution, [status(thm)], [d37,d25])).
% 15.01/8.77 cnf(d39, plain, ia != ia | 'Ts24' | sK28 = ib | sK28 = ia, inference(superposition, [status(thm)], [d38,c30])).
% 15.01/8.77 cnf(d40, plain, sK28 = ib | sK28 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d39])).
% 15.01/8.77 cnf(d41, plain, sK28 = ib | sK28 = ia | sK28 = ib | sK28 = ia, inference(resolution, [status(thm)], [d40,d25])).
% 15.01/8.77 cnf(d42, plain, ~requalityOnA(ib,sK27) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | sK28 = ia, inference(superposition, [status(thm)], [d41,d8])).
% 15.01/8.77 cnf(d43, plain, sK28 = ia | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ib,sK27) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d42])).
% 15.01/8.77 cnf(d44, plain, ~requalityOnA(X0,ib) | X0 = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | sK28 = ia, inference(superposition, [status(thm)], [d41,d5])).
% 15.01/8.77 cnf(d45, plain, X0 = sK27 | sK28 = ia | ~cowlThing(sK25) | ~requalityOnA(X0,ib) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d44])).
% 15.01/8.77 cnf(d46, plain, ib = sK27 | sK28 = ia | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d45,c19])).
% 15.01/8.77 cnf(d47, plain, ib = sK27 | sK28 = ia | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d46])).
% 15.01/8.77 cnf(d48, plain, ib = sK27 | sK28 = ia | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d47,c10])).
% 15.01/8.77 cnf(d49, plain, ~cowlThing(ic) | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | X0 = sK27 | ~requalityOnA(X0,sK28), inference(resolution, [status(thm)], [d18,c14])).
% 15.01/8.77 cnf(d50, plain, X0 = sK27 | ~cowlThing(sK25) | ~requalityOnA(X0,sK28) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d49])).
% 15.01/8.77 cnf(d51, plain, ~requalityOnA(X0,ib) | X0 = sK27 | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | sK28 = ia, inference(superposition, [status(thm)], [d41,d50])).
% 15.01/8.77 cnf(d52, plain, X0 = sK27 | sK28 = ia | ~requalityOnA(X0,ib) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d51])).
% 15.01/8.77 cnf(d53, plain, ib = sK27 | sK28 = ia | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d52,c19])).
% 15.01/8.77 cnf(d54, plain, ib = sK27 | sK28 = ia | 'xsd$ustring'(sK26) | ~'Ts24' | ib = sK27 | sK28 = ia | ~'Ts24', inference(resolution, [status(thm)], [d53,d48])).
% 15.01/8.77 cnf(d55, plain, ib = sK27 | sK28 = ia | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d54,c9])).
% 15.01/8.77 cnf(d56, plain, ib = sK27 | sK28 = ia | ~'Ts24' | ib = sK27 | sK28 = ia | ~'Ts24', inference(resolution, [status(thm)], [d55,d48])).
% 15.01/8.77 cnf(d57, plain, X0 = sK29 | ~requalityOnA(X0,sK30) | 'Ts24', inference(resolution, [status(thm)], [c14,c29])).
% 15.01/8.77 cnf(d58, plain, ib = sK27 | sK28 = ia | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d56,d28])).
% 15.01/8.77 cnf(d59, plain, ~requalityOnA(X0,ib) | X0 = sK29 | 'Ts24' | ib = sK27 | sK28 = ia | sK30 = ia, inference(superposition, [status(thm)], [d58,d57])).
% 15.01/8.77 cnf(d60, plain, ib = sK29 | ib = sK27 | sK28 = ia | sK30 = ia | 'Ts24', inference(resolution, [status(thm)], [d59,c19])).
% 15.01/8.77 cnf(d61, plain, ib = sK27 | ib = sK29 | sK28 = ia | sK30 = ia | ib = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d60,d56])).
% 15.01/8.77 cnf(d62, plain, requalityOnA(sK29,ia) | 'Ts24' | ib = sK27 | ib = sK29 | sK28 = ia, inference(superposition, [status(thm)], [d61,c29])).
% 15.01/8.77 cnf(d63, plain, ib = sK27 | ib = sK29 | sK28 = ia | 'Ts24' | sK29 = ia, inference(resolution, [status(thm)], [d62,d0])).
% 15.01/8.77 cnf(d64, plain, ib = sK27 | ib = sK29 | sK28 = ia | sK29 = ia | ib = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d63,d56])).
% 15.01/8.77 cnf(d65, plain, ib != ib | 'Ts24' | ib = sK27 | sK28 = ia | sK29 = ia, inference(superposition, [status(thm)], [d64,c31])).
% 15.01/8.77 cnf(d66, plain, ib = sK27 | sK28 = ia | sK29 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d65])).
% 15.01/8.77 cnf(d67, plain, ib = sK27 | sK28 = ia | sK29 = ia | ib = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d66,d56])).
% 15.01/8.77 cnf(d68, plain, ia != ia | 'Ts24' | ib = sK27 | sK28 = ia, inference(superposition, [status(thm)], [d67,c30])).
% 15.01/8.77 cnf(d69, plain, ib = sK27 | sK28 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d68])).
% 15.01/8.77 cnf(d70, plain, ib = sK27 | sK28 = ia | ib = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d69,d56])).
% 15.01/8.77 cnf(d71, plain, ~requalityOnA(X0,ia) | X0 = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ib = sK27, inference(superposition, [status(thm)], [d70,d5])).
% 15.01/8.77 cnf(d72, plain, X0 = sK27 | ib = sK27 | ~cowlThing(sK25) | ~requalityOnA(X0,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d71])).
% 15.01/8.77 cnf(d73, plain, ia = sK27 | ib = sK27 | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d72,c17])).
% 15.01/8.77 cnf(d74, plain, ib = sK27 | ia = sK27 | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d73])).
% 15.01/8.77 cnf(d75, plain, ib = sK27 | ia = sK27 | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d74,c10])).
% 15.01/8.77 cnf(d76, plain, ~requalityOnA(X0,ia) | X0 = sK27 | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ib = sK27, inference(superposition, [status(thm)], [d70,d50])).
% 15.01/8.77 cnf(d77, plain, X0 = sK27 | ib = sK27 | ~requalityOnA(X0,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d76])).
% 15.01/8.77 cnf(d78, plain, ia = sK27 | ib = sK27 | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d77,c17])).
% 15.01/8.77 cnf(d79, plain, ib = sK27 | ia = sK27 | ~'Ts24' | ib = sK27 | ia = sK27 | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d75,d78])).
% 15.01/8.77 cnf(d80, plain, ib = sK27 | ia = sK27 | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d79,c9])).
% 15.01/8.77 cnf(d81, plain, ib = sK27 | ia = sK27 | ~'Ts24' | ib = sK27 | ia = sK27 | ~'Ts24', inference(resolution, [status(thm)], [d80,d75])).
% 15.01/8.77 cnf(d82, plain, ib = sK27 | ia = sK27 | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d81,d28])).
% 15.01/8.77 cnf(d83, plain, ~requalityOnA(X0,ib) | X0 = sK29 | 'Ts24' | ib = sK27 | ia = sK27 | sK30 = ia, inference(superposition, [status(thm)], [d82,d57])).
% 15.01/8.77 cnf(d84, plain, ib = sK29 | ib = sK27 | ia = sK27 | sK30 = ia | 'Ts24', inference(resolution, [status(thm)], [d83,c19])).
% 15.01/8.77 cnf(d85, plain, ib = sK27 | ib = sK29 | ia = sK27 | sK30 = ia | ib = sK27 | ia = sK27, inference(resolution, [status(thm)], [d84,d81])).
% 15.01/8.77 cnf(d86, plain, ~requalityOnA(X0,ia) | X0 = sK29 | 'Ts24' | ib = sK27 | ib = sK29 | ia = sK27, inference(superposition, [status(thm)], [d85,d57])).
% 15.01/8.77 cnf(d87, plain, ia = sK29 | ib = sK27 | ib = sK29 | ia = sK27 | 'Ts24', inference(resolution, [status(thm)], [d86,c17])).
% 15.01/8.77 cnf(d88, plain, ib = sK27 | ib = sK29 | ia = sK27 | ia = sK29 | ib = sK27 | ia = sK27, inference(resolution, [status(thm)], [d87,d81])).
% 15.01/8.77 cnf(d89, plain, ib != ib | 'Ts24' | ib = sK27 | ia = sK27 | ia = sK29, inference(superposition, [status(thm)], [d88,c31])).
% 15.01/8.77 cnf(d90, plain, ib = sK27 | ia = sK27 | ia = sK29 | 'Ts24', inference(equality_resolution, [status(thm)], [d89])).
% 15.01/8.77 cnf(d91, plain, ib = sK27 | ia = sK27 | ia = sK29 | ib = sK27 | ia = sK27, inference(resolution, [status(thm)], [d90,d81])).
% 15.01/8.77 cnf(d92, plain, ia != ia | 'Ts24' | ib = sK27 | ia = sK27, inference(superposition, [status(thm)], [d91,c30])).
% 15.01/8.77 cnf(d93, plain, ib = sK27 | ia = sK27 | 'Ts24', inference(equality_resolution, [status(thm)], [d92])).
% 15.01/8.77 cnf(d94, plain, ib = sK27 | ia = sK27 | ib = sK27 | ia = sK27, inference(resolution, [status(thm)], [d93,d81])).
% 15.01/8.77 cnf(d95, plain, ~requalityOnA(ib,ib) | sK28 = ia | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d94,d43])).
% 15.01/8.77 cnf(d96, plain, ia = sK27 | sK28 = ia | ~cowlThing(sK25) | ~requalityOnA(ib,ib) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d95])).
% 15.01/8.77 cnf(d97, plain, ia = sK27 | sK28 = ia | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c19,d96])).
% 15.01/8.77 cnf(d98, plain, ia = sK27 | sK28 = ia | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d97,c10])).
% 15.01/8.77 cnf(d99, plain, ia = sK27 | sK28 = ia | 'xsd$uinteger'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d98])).
% 15.01/8.77 cnf(d100, plain, cowlNothing(sK25) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | ~requalityOnA(sK28,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,c24])).
% 15.01/8.77 cnf(d101, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | ~requalityOnA(sK28,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c8,d100])).
% 15.01/8.77 cnf(d102, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(sK28,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d101])).
% 15.01/8.77 cnf(d103, plain, ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(sK28,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d102])).
% 15.01/8.77 cnf(d104, plain, ~requalityOnA(ib,sK27) | ~cowlThing(ic) | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | sK28 = ia, inference(superposition, [status(thm)], [d41,d103])).
% 15.01/8.77 cnf(d105, plain, sK28 = ia | ~cowlThing(sK25) | ~requalityOnA(ib,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d104])).
% 15.01/8.77 cnf(d106, plain, ~requalityOnA(ib,ib) | sK28 = ia | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d94,d105])).
% 15.01/8.77 cnf(d107, plain, ia = sK27 | sK28 = ia | ~requalityOnA(ib,ib) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d106])).
% 15.01/8.77 cnf(d108, plain, ia = sK27 | sK28 = ia | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c19,d107])).
% 15.01/8.77 cnf(d109, plain, ia = sK27 | sK28 = ia | 'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27 | sK28 = ia | ~'Ts24', inference(resolution, [status(thm)], [d108,d99])).
% 15.01/8.77 cnf(d110, plain, ia = sK27 | sK28 = ia | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d109,c9])).
% 15.01/8.77 cnf(d111, plain, ia = sK27 | sK28 = ia | ~'Ts24' | ia = sK27 | sK28 = ia | ~'Ts24', inference(resolution, [status(thm)], [d110,d99])).
% 15.01/8.77 cnf(d112, plain, ia = sK27 | sK28 = ia | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d111,d28])).
% 15.01/8.77 cnf(d113, plain, requalityOnA(sK29,ib) | 'Ts24' | ia = sK27 | sK28 = ia | sK30 = ia, inference(superposition, [status(thm)], [d112,c29])).
% 15.01/8.77 cnf(d114, plain, ia = sK27 | sK28 = ia | sK30 = ia | 'Ts24' | sK29 = ib, inference(resolution, [status(thm)], [d113,d26])).
% 15.01/8.77 cnf(d115, plain, ia = sK27 | sK28 = ia | sK29 = ib | sK30 = ia | ia = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d114,d111])).
% 15.01/8.77 cnf(d116, plain, requalityOnA(sK29,ia) | 'Ts24' | ia = sK27 | sK28 = ia | sK29 = ib, inference(superposition, [status(thm)], [d115,c29])).
% 15.01/8.77 cnf(d117, plain, ia = sK27 | sK28 = ia | sK29 = ib | 'Ts24' | sK29 = ia, inference(resolution, [status(thm)], [d116,d0])).
% 15.01/8.77 cnf(d118, plain, ia = sK27 | sK28 = ia | sK29 = ib | sK29 = ia | ia = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d117,d111])).
% 15.01/8.77 cnf(d119, plain, ib != ib | 'Ts24' | ia = sK27 | sK28 = ia | sK29 = ia, inference(superposition, [status(thm)], [d118,c31])).
% 15.01/8.77 cnf(d120, plain, ia = sK27 | sK28 = ia | sK29 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d119])).
% 15.01/8.77 cnf(d121, plain, ia = sK27 | sK28 = ia | sK29 = ia | ia = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d120,d111])).
% 15.01/8.77 cnf(d122, plain, ia != ia | 'Ts24' | ia = sK27 | sK28 = ia, inference(superposition, [status(thm)], [d121,c30])).
% 15.01/8.77 cnf(d123, plain, ia = sK27 | sK28 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d122])).
% 15.01/8.77 cnf(d124, plain, ia = sK27 | sK28 = ia | ia = sK27 | sK28 = ia, inference(resolution, [status(thm)], [d123,d111])).
% 15.01/8.77 cnf(d125, plain, ~requalityOnA(X0,ia) | X0 = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d124,d5])).
% 15.01/8.77 cnf(d126, plain, X0 = sK27 | ia = sK27 | ~cowlThing(sK25) | ~requalityOnA(X0,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d125])).
% 15.01/8.77 cnf(d127, plain, ia = sK27 | ia = sK27 | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d126,c17])).
% 15.01/8.77 cnf(d128, plain, ia = sK27 | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d127])).
% 15.01/8.77 cnf(d129, plain, ia = sK27 | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d128,c10])).
% 15.01/8.77 cnf(d130, plain, ~requalityOnA(X0,ia) | X0 = sK27 | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d124,d50])).
% 15.01/8.77 cnf(d131, plain, X0 = sK27 | ia = sK27 | ~requalityOnA(X0,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d130])).
% 15.01/8.77 cnf(d132, plain, ia = sK27 | ia = sK27 | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d131,c17])).
% 15.01/8.77 cnf(d133, plain, ia = sK27 | ~'Ts24' | ia = sK27 | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d129,d132])).
% 15.01/8.77 cnf(d134, plain, ia = sK27 | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d133,c9])).
% 15.01/8.77 cnf(d135, plain, ia = sK27 | ~'Ts24' | ia = sK27 | ~'Ts24', inference(resolution, [status(thm)], [d134,d129])).
% 15.01/8.77 cnf(d136, plain, ia = sK27 | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d135,d28])).
% 15.01/8.77 cnf(d137, plain, requalityOnA(sK29,ib) | 'Ts24' | ia = sK27 | sK30 = ia, inference(superposition, [status(thm)], [d136,c29])).
% 15.01/8.77 cnf(d138, plain, ia = sK27 | sK30 = ia | 'Ts24' | sK29 = ib, inference(resolution, [status(thm)], [d137,d26])).
% 15.01/8.77 cnf(d139, plain, ia = sK27 | sK29 = ib | sK30 = ia | ia = sK27, inference(resolution, [status(thm)], [d138,d135])).
% 15.01/8.77 cnf(d140, plain, requalityOnA(sK29,ia) | 'Ts24' | ia = sK27 | sK29 = ib, inference(superposition, [status(thm)], [d139,c29])).
% 15.01/8.77 cnf(d141, plain, ia = sK27 | sK29 = ib | 'Ts24' | sK29 = ia, inference(resolution, [status(thm)], [d140,d0])).
% 15.01/8.77 cnf(d142, plain, ia = sK27 | sK29 = ib | sK29 = ia | ia = sK27, inference(resolution, [status(thm)], [d141,d135])).
% 15.01/8.77 cnf(d143, plain, ib != ib | 'Ts24' | ia = sK27 | sK29 = ia, inference(superposition, [status(thm)], [d142,c31])).
% 15.01/8.77 cnf(d144, plain, ia = sK27 | sK29 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d143])).
% 15.01/8.77 cnf(d145, plain, ia = sK27 | sK29 = ia | ia = sK27, inference(resolution, [status(thm)], [d144,d135])).
% 15.01/8.77 cnf(d146, plain, ia != ia | 'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d145,c30])).
% 15.01/8.77 cnf(d147, plain, ia = sK27 | 'Ts24', inference(equality_resolution, [status(thm)], [d146])).
% 15.01/8.77 cnf(d148, plain, ia = sK27 | ia = sK27, inference(resolution, [status(thm)], [d147,d135])).
% 15.01/8.77 cnf(d149, plain, ~requalityOnA(ia,sK27) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ib = sK27, inference(superposition, [status(thm)], [d70,d8])).
% 15.01/8.77 cnf(d150, plain, ib = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,sK27) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d149])).
% 15.01/8.77 cnf(d151, plain, requalityOnA(ib,sK28) | ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d94,d3])).
% 15.01/8.77 cnf(d152, plain, ia = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | requalityOnA(ib,sK28) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d151])).
% 15.01/8.77 cnf(d153, plain, requalityOnA(ib,ia) | ia = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d124,d152])).
% 15.01/8.77 cnf(d154, plain, ia = sK27 | ~cowlThing(sK25) | requalityOnA(ib,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d153])).
% 15.01/8.77 cnf(d155, plain, ia = sK27 | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ib = ia, inference(resolution, [status(thm)], [d154,d0])).
% 15.01/8.77 cnf(d156, plain, ib = ia | ia = sK27 | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d155])).
% 15.01/8.77 cnf(d157, plain, ib = ia | ia = sK27 | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d156,c10])).
% 15.01/8.77 cnf(d158, plain, requalityOnA(ib,sK28) | ~cowlThing(ic) | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d94,d18])).
% 15.01/8.77 cnf(d159, plain, ia = sK27 | ~cowlThing(sK25) | requalityOnA(ib,sK28) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d158])).
% 15.01/8.77 cnf(d160, plain, requalityOnA(ib,ia) | ia = sK27 | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ia = sK27, inference(superposition, [status(thm)], [d124,d159])).
% 15.01/8.77 cnf(d161, plain, ia = sK27 | requalityOnA(ib,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d160])).
% 15.01/8.77 cnf(d162, plain, ia = sK27 | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ib = ia, inference(resolution, [status(thm)], [d161,d0])).
% 15.01/8.77 cnf(d163, plain, ib = ia | ia = sK27 | ~'Ts24' | ib = ia | ia = sK27 | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d157,d162])).
% 15.01/8.77 cnf(d164, plain, ib = ia | ia = sK27 | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d163,c9])).
% 15.01/8.77 cnf(d165, plain, ib = ia | ia = sK27 | ~'Ts24' | ib = ia | ia = sK27 | ~'Ts24', inference(resolution, [status(thm)], [d164,d157])).
% 15.01/8.77 cnf(d166, plain, ib = ia | ia = sK27 | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d165,d28])).
% 15.01/8.77 cnf(d167, plain, requalityOnA(sK29,ib) | 'Ts24' | ib = ia | ia = sK27 | sK30 = ia, inference(superposition, [status(thm)], [d166,c29])).
% 15.01/8.77 cnf(d168, plain, ib = ia | ia = sK27 | sK30 = ia | 'Ts24' | sK29 = ib, inference(resolution, [status(thm)], [d167,d26])).
% 15.01/8.77 cnf(d169, plain, ib = ia | ia = sK27 | sK29 = ib | sK30 = ia | ib = ia | ia = sK27, inference(resolution, [status(thm)], [d168,d165])).
% 15.01/8.77 cnf(d170, plain, requalityOnA(sK29,ia) | 'Ts24' | ib = ia | ia = sK27 | sK29 = ib, inference(superposition, [status(thm)], [d169,c29])).
% 15.01/8.77 cnf(d171, plain, ib = ia | ia = sK27 | sK29 = ib | 'Ts24' | sK29 = ia, inference(resolution, [status(thm)], [d170,d0])).
% 15.01/8.77 cnf(d172, plain, ib = ia | ia = sK27 | sK29 = ib | sK29 = ia | ib = ia | ia = sK27, inference(resolution, [status(thm)], [d171,d165])).
% 15.01/8.77 cnf(d173, plain, ib != ib | 'Ts24' | ib = ia | ia = sK27 | sK29 = ia, inference(superposition, [status(thm)], [d172,c31])).
% 15.01/8.77 cnf(d174, plain, ib = ia | ia = sK27 | sK29 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d173])).
% 15.01/8.77 cnf(d175, plain, ib = ia | ia = sK27 | sK29 = ia | ib = ia | ia = sK27, inference(resolution, [status(thm)], [d174,d165])).
% 15.01/8.77 cnf(d176, plain, ia != ia | 'Ts24' | ib = ia | ia = sK27, inference(superposition, [status(thm)], [d175,c30])).
% 15.01/8.77 cnf(d177, plain, ib = ia | ia = sK27 | 'Ts24', inference(equality_resolution, [status(thm)], [d176])).
% 15.01/8.77 cnf(d178, plain, ib = ia | ia = sK27 | ib = ia | ia = sK27, inference(resolution, [status(thm)], [d177,d165])).
% 15.01/8.77 cnf(d179, plain, ~requalityOnA(ia,ia) | ib = sK27 | ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24' | ib = ia, inference(superposition, [status(thm)], [d178,d150])).
% 15.01/8.77 cnf(d180, plain, ib = ia | ib = ia | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d179,d148])).
% 15.01/8.77 cnf(d181, plain, ib = ia | ib = ia | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d180])).
% 15.01/8.77 cnf(d182, plain, ib = ia | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d181])).
% 15.01/8.77 cnf(d183, plain, ib = ia | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d182,c10])).
% 15.01/8.77 cnf(d184, plain, ib = ia | 'xsd$uinteger'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d183])).
% 15.01/8.77 cnf(d185, plain, ~requalityOnA(ia,sK27) | ~cowlThing(ic) | ~cowlThing(sK25) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24' | ib = sK27, inference(superposition, [status(thm)], [d70,d103])).
% 15.01/8.77 cnf(d186, plain, ib = sK27 | ~cowlThing(sK25) | ~requalityOnA(ia,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d185])).
% 15.01/8.77 cnf(d187, plain, ib = ia | ~cowlThing(sK25) | ~requalityOnA(ia,sK27) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d186,d148])).
% 15.01/8.77 cnf(d188, plain, ib = ia | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d187,d148])).
% 15.01/8.77 cnf(d189, plain, ib = ia | ~requalityOnA(ia,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d188])).
% 15.01/8.77 cnf(d190, plain, ib = ia | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d189])).
% 15.01/8.77 cnf(d191, plain, ib = ia | ~'Ts24' | ib = ia | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d184,d190])).
% 15.01/8.77 cnf(d192, plain, ib = ia | ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d191,c9])).
% 15.01/8.77 cnf(d193, plain, ib = ia | ~'Ts24' | ib = ia | ~'Ts24', inference(resolution, [status(thm)], [d192,d184])).
% 15.01/8.77 cnf(d194, plain, ib = ia | sK30 = ib | sK30 = ia, inference(resolution, [status(thm)], [d193,d28])).
% 15.01/8.77 cnf(d195, plain, requalityOnA(sK29,ib) | 'Ts24' | ib = ia | sK30 = ia, inference(superposition, [status(thm)], [d194,c29])).
% 15.01/8.77 cnf(d196, plain, ib = ia | sK30 = ia | 'Ts24' | sK29 = ib, inference(resolution, [status(thm)], [d195,d26])).
% 15.01/8.77 cnf(d197, plain, ib = ia | sK29 = ib | sK30 = ia | ib = ia, inference(resolution, [status(thm)], [d196,d193])).
% 15.01/8.77 cnf(d198, plain, requalityOnA(sK29,ia) | 'Ts24' | ib = ia | sK29 = ib, inference(superposition, [status(thm)], [d197,c29])).
% 15.01/8.77 cnf(d199, plain, ib = ia | sK29 = ib | 'Ts24' | sK29 = ia, inference(resolution, [status(thm)], [d198,d0])).
% 15.01/8.77 cnf(d200, plain, ib = ia | sK29 = ib | sK29 = ia | ib = ia, inference(resolution, [status(thm)], [d199,d193])).
% 15.01/8.77 cnf(d201, plain, ib != ib | 'Ts24' | ib = ia | sK29 = ia, inference(superposition, [status(thm)], [d200,c31])).
% 15.01/8.77 cnf(d202, plain, ib = ia | sK29 = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d201])).
% 15.01/8.77 cnf(d203, plain, ib = ia | sK29 = ia | ib = ia, inference(resolution, [status(thm)], [d202,d193])).
% 15.01/8.77 cnf(d204, plain, ia != ia | 'Ts24' | ib = ia, inference(superposition, [status(thm)], [d203,c30])).
% 15.01/8.77 cnf(d205, plain, ib = ia | 'Ts24', inference(equality_resolution, [status(thm)], [d204])).
% 15.01/8.77 cnf(d206, plain, ib = ia | ib = ia, inference(resolution, [status(thm)], [d205,d193])).
% 15.01/8.77 cnf(d207, plain, sK30 = ia | sK30 = ia | 'Ts24', inference(demodulation, [status(thm)], [d28,d206])).
% 15.01/8.77 cnf(d208, plain, sK28 = ia | sK28 = ia, inference(demodulation, [status(thm)], [d41,d206])).
% 15.01/8.77 cnf(d209, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(sK28,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d8,d148])).
% 15.01/8.77 cnf(d210, plain, ~cowlThing(ia) | ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d209,d208])).
% 15.01/8.77 cnf(d211, plain, ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(ia,ia) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d210])).
% 15.01/8.77 cnf(d212, plain, ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d211])).
% 15.01/8.77 cnf(d213, plain, ~cowlThing(ic) | ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'Ts24' | 'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d212,c10])).
% 15.01/8.77 cnf(d214, plain, ~cowlThing(sK25) | 'xsd$uinteger'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d213])).
% 15.01/8.77 cnf(d215, plain, 'xsd$uinteger'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d214,c7])).
% 15.01/8.77 cnf(d216, plain, ~cowlThing(ic) | ~cowlThing(sK25) | ~requalityOnA(sK28,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d103,d148])).
% 15.01/8.77 cnf(d217, plain, ~cowlThing(sK25) | ~requalityOnA(sK28,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d216])).
% 15.01/8.77 cnf(d218, plain, ~cowlThing(sK25) | ~requalityOnA(ia,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(demodulation, [status(thm)], [d217,d208])).
% 15.01/8.77 cnf(d219, plain, ~requalityOnA(ia,ia) | ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c7,d218])).
% 15.01/8.77 cnf(d220, plain, ~'xsd$uinteger'(sK26) | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [c17,d219])).
% 15.01/8.77 cnf(d221, plain, ~'Ts24' | 'xsd$ustring'(sK26) | ~'Ts24', inference(resolution, [status(thm)], [d215,d220])).
% 15.01/8.77 cnf(d222, plain, ~'Ts24' | ~'xsd$uinteger'(sK26), inference(resolution, [status(thm)], [d221,c9])).
% 15.01/8.77 cnf(d223, plain, ~'Ts24' | ~'Ts24', inference(resolution, [status(thm)], [d222,d215])).
% 15.01/8.77 cnf(d224, plain, sK30 = ia, inference(resolution, [status(thm)], [d223,d207])).
% 15.01/8.77 cnf(d225, plain, requalityOnA(sK29,sK30), inference(resolution, [status(thm)], [d223,c29])).
% 15.01/8.77 cnf(d226, plain, requalityOnA(sK29,ia), inference(demodulation, [status(thm)], [d225,d224])).
% 15.01/8.77 cnf(d227, plain, sK29 = ia, inference(resolution, [status(thm)], [d226,d0])).
% 15.01/8.77 cnf(d228, plain, sK29 != ia, inference(resolution, [status(thm)], [d223,c30])).
% 15.01/8.77 cnf(d229, plain, $false, inference(resolution, [status(thm)], [d228,d227])).
% 15.01/8.77 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------