%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR045+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 : Thu Sep 24 12:14:46 PM UTC 2026
% Result : Theorem 0.13s 5.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR045+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n007.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 14:30:55 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.13/5.40 % Drodi V4.1.1
% 0.13/5.46 % Refutation found
% 0.13/5.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.46 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.46 fof(f13,axiom,(
% 0.13/5.46 (! [ARG1,ARG2] :( subsetof(ARG1,ARG2)=> most(ARG1,ARG2) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f33,axiom,(
% 0.13/5.46 (! [OBJ] :( partiallyintangibleindividual(OBJ)=> individual(OBJ) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f83,axiom,(
% 0.13/5.46 applicationcontext(c_wamt_evalinitial_p14) ),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f156,axiom,(
% 0.13/5.46 (! [OBJ] :( microtheory(OBJ)=> aspatialinformationstore(OBJ) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f167,axiom,(
% 0.13/5.46 (! [OBJ] :~ ( individual(OBJ)& setorcollection(OBJ) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f171,axiom,(
% 0.13/5.46 (! [OBJ] :( applicationcontext(OBJ)=> microtheory(OBJ) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f264,axiom,(
% 0.13/5.46 (! [ARG1,ARG2] :( most(ARG1,ARG2)=> setorcollection(ARG1) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f320,axiom,(
% 0.13/5.46 (! [OBJ] :( intangibleindividual(OBJ)=> partiallyintangibleindividual(OBJ) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f382,axiom,(
% 0.13/5.46 (! [OBJ] :( aspatialinformationstore(OBJ)=> intangibleindividual(OBJ) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f413,axiom,(
% 0.13/5.46 (! [ARG1,ARG2] :( genls(ARG1,ARG2)=> subsetof(ARG1,ARG2) ) )),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f1132,conjecture,(
% 0.13/5.46 ~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088) ),
% 0.13/5.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.46 fof(f1133,negated_conjecture,(
% 0.13/5.46 ~(~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088) )),
% 0.13/5.46 inference(negated_conjecture,[status(cth)],[f1132])).
% 0.13/5.46 fof(f1152,plain,(
% 0.13/5.46 ![ARG1,ARG2]: (~subsetof(ARG1,ARG2)|most(ARG1,ARG2))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.13/5.46 fof(f1153,plain,(
% 0.13/5.46 ![X0,X1]: (~subsetof(X0,X1)|most(X0,X1))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1152])).
% 0.13/5.46 fof(f1182,plain,(
% 0.13/5.46 ![OBJ]: (~partiallyintangibleindividual(OBJ)|individual(OBJ))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.13/5.46 fof(f1183,plain,(
% 0.13/5.46 ![X0]: (~partiallyintangibleindividual(X0)|individual(X0))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1182])).
% 0.13/5.46 fof(f1255,plain,(
% 0.13/5.46 applicationcontext(c_wamt_evalinitial_p14)),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f83])).
% 0.13/5.46 fof(f1358,plain,(
% 0.13/5.46 ![OBJ]: (~microtheory(OBJ)|aspatialinformationstore(OBJ))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f156])).
% 0.13/5.46 fof(f1359,plain,(
% 0.13/5.46 ![X0]: (~microtheory(X0)|aspatialinformationstore(X0))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1358])).
% 0.13/5.46 fof(f1377,plain,(
% 0.13/5.46 ![OBJ]: (~individual(OBJ)|~setorcollection(OBJ))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f167])).
% 0.13/5.46 fof(f1378,plain,(
% 0.13/5.46 ![X0]: (~individual(X0)|~setorcollection(X0))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1377])).
% 0.13/5.46 fof(f1383,plain,(
% 0.13/5.46 ![OBJ]: (~applicationcontext(OBJ)|microtheory(OBJ))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f171])).
% 0.13/5.46 fof(f1384,plain,(
% 0.13/5.46 ![X0]: (~applicationcontext(X0)|microtheory(X0))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1383])).
% 0.13/5.46 fof(f1517,plain,(
% 0.13/5.46 ![ARG1,ARG2]: (~most(ARG1,ARG2)|setorcollection(ARG1))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f264])).
% 0.13/5.46 fof(f1518,plain,(
% 0.13/5.46 ![ARG1]: ((![ARG2]: ~most(ARG1,ARG2))|setorcollection(ARG1))),
% 0.13/5.46 inference(miniscoping,[status(thm)],[f1517])).
% 0.13/5.46 fof(f1519,plain,(
% 0.13/5.46 ![X0,X1]: (~most(X0,X1)|setorcollection(X0))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1518])).
% 0.13/5.46 fof(f1601,plain,(
% 0.13/5.46 ![OBJ]: (~intangibleindividual(OBJ)|partiallyintangibleindividual(OBJ))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f320])).
% 0.13/5.46 fof(f1602,plain,(
% 0.13/5.46 ![X0]: (~intangibleindividual(X0)|partiallyintangibleindividual(X0))),
% 0.13/5.46 inference(cnf_transformation,[status(thm)],[f1601])).
% 0.13/5.46 fof(f1689,plain,(
% 0.13/5.46 ![OBJ]: (~aspatialinformationstore(OBJ)|intangibleindividual(OBJ))),
% 0.13/5.46 inference(pre_NNF_transformation,[status(thm)],[f382])).
% 0.13/5.47 fof(f1690,plain,(
% 0.13/5.47 ![X0]: (~aspatialinformationstore(X0)|intangibleindividual(X0))),
% 0.13/5.47 inference(cnf_transformation,[status(thm)],[f1689])).
% 0.13/5.47 fof(f1735,plain,(
% 0.13/5.47 ![ARG1,ARG2]: (~genls(ARG1,ARG2)|subsetof(ARG1,ARG2))),
% 0.13/5.47 inference(pre_NNF_transformation,[status(thm)],[f413])).
% 0.13/5.47 fof(f1736,plain,(
% 0.13/5.47 ![X0,X1]: (~genls(X0,X1)|subsetof(X0,X1))),
% 0.13/5.47 inference(cnf_transformation,[status(thm)],[f1735])).
% 0.13/5.47 fof(f3204,plain,(
% 0.13/5.47 genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088)),
% 0.13/5.47 inference(cnf_transformation,[status(thm)],[f1133])).
% 0.13/5.47 fof(f3485,plain,(
% 0.13/5.47 ![X0]: (~applicationcontext(X0)|aspatialinformationstore(X0))),
% 0.13/5.47 inference(resolution,[status(thm)],[f1384,f1359])).
% 0.13/5.47 fof(f3767,plain,(
% 0.13/5.47 subsetof(c_wamt_evalinitial_p14,c_tptpcol_15_80088)),
% 0.13/5.47 inference(resolution,[status(thm)],[f1736,f3204])).
% 0.13/5.47 fof(f3769,plain,(
% 0.13/5.47 most(c_wamt_evalinitial_p14,c_tptpcol_15_80088)),
% 0.13/5.47 inference(resolution,[status(thm)],[f3767,f1153])).
% 0.13/5.47 fof(f3779,plain,(
% 0.13/5.47 setorcollection(c_wamt_evalinitial_p14)),
% 0.13/5.47 inference(resolution,[status(thm)],[f3769,f1519])).
% 0.13/5.47 fof(f3780,plain,(
% 0.13/5.47 ~individual(c_wamt_evalinitial_p14)),
% 0.13/5.47 inference(resolution,[status(thm)],[f3779,f1378])).
% 0.13/5.47 fof(f3782,plain,(
% 0.13/5.47 ~partiallyintangibleindividual(c_wamt_evalinitial_p14)),
% 0.13/5.47 inference(resolution,[status(thm)],[f3780,f1183])).
% 0.13/5.47 fof(f4442,plain,(
% 0.13/5.47 aspatialinformationstore(c_wamt_evalinitial_p14)),
% 0.13/5.47 inference(resolution,[status(thm)],[f3485,f1255])).
% 0.13/5.47 fof(f4447,plain,(
% 0.13/5.47 intangibleindividual(c_wamt_evalinitial_p14)),
% 0.13/5.47 inference(resolution,[status(thm)],[f4442,f1690])).
% 0.13/5.47 fof(f4449,plain,(
% 0.13/5.47 partiallyintangibleindividual(c_wamt_evalinitial_p14)),
% 0.13/5.47 inference(resolution,[status(thm)],[f4447,f1602])).
% 0.13/5.47 fof(f4450,plain,(
% 0.13/5.47 $false),
% 0.13/5.47 inference(forward_subsumption_resolution,[status(thm)],[f4449,f3782])).
% 0.13/5.47 % SZS output end CNFRefutation for theBenchmark.p
% 1.46/6.69 % Elapsed time: 1.097964 seconds
% 1.46/6.69 % CPU time: 0.381876 seconds
% 1.46/6.69 % Total memory used: 93.991 MB
% 1.46/6.69 % Net memory used: 93.679 MB
%------------------------------------------------------------------------------