%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR045+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:13:06 PM UTC 2026
% Result : Theorem 97.98s 13.81s
% Output : CNFRefutation 91.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of formulae : 35 ( 10 unt; 0 def)
% Number of atoms : 60 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 50 ( 25 ~; 18 |; 1 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 29 ( 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f567,axiom,
! [OBJ] :
( applicationcontext(OBJ)
=> microtheory(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4028,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5173,axiom,
! [OBJ] :
( microtheory(OBJ)
=> aspatialinformationstore(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6118,axiom,
! [OBJ] :
( aspatialinformationstore(OBJ)
=> intangibleindividual(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6724,axiom,
applicationcontext(c_wamt_evalinitial_p14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10185,axiom,
! [OBJ] :
( partiallyintangibleindividual(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16874,axiom,
! [OBJ] :
( intangibleindividual(OBJ)
=> partiallyintangibleindividual(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19537,axiom,
! [ARG1,ARG2] :
( genls(ARG1,ARG2)
=> collection(ARG1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44217,conjecture,
~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44218,negated_conjecture,
~ ~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f44911,plain,
! [OBJ] :
( microtheory(OBJ)
| ~ applicationcontext(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f567]) ).
fof(f44912,plain,
! [X0] :
( microtheory(X0)
| ~ applicationcontext(X0) ),
inference(cnf_transformation,[status(thm)],[f44911]) ).
fof(f49265,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f4028]) ).
fof(f49266,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(thm)],[f49265]) ).
fof(f50694,plain,
! [OBJ] :
( aspatialinformationstore(OBJ)
| ~ microtheory(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f5173]) ).
fof(f50695,plain,
! [X0] :
( aspatialinformationstore(X0)
| ~ microtheory(X0) ),
inference(cnf_transformation,[status(thm)],[f50694]) ).
fof(f51909,plain,
! [OBJ] :
( intangibleindividual(OBJ)
| ~ aspatialinformationstore(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f6118]) ).
fof(f51910,plain,
! [X0] :
( intangibleindividual(X0)
| ~ aspatialinformationstore(X0) ),
inference(cnf_transformation,[status(thm)],[f51909]) ).
fof(f52658,plain,
applicationcontext(c_wamt_evalinitial_p14),
inference(cnf_transformation,[status(thm)],[f6724]) ).
fof(f57019,plain,
! [OBJ] :
( individual(OBJ)
| ~ partiallyintangibleindividual(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f10185]) ).
fof(f57020,plain,
! [X0] :
( individual(X0)
| ~ partiallyintangibleindividual(X0) ),
inference(cnf_transformation,[status(thm)],[f57019]) ).
fof(f65391,plain,
! [OBJ] :
( partiallyintangibleindividual(OBJ)
| ~ intangibleindividual(OBJ) ),
inference(pre_NNF_transformation,[status(thm)],[f16874]) ).
fof(f65392,plain,
! [X0] :
( partiallyintangibleindividual(X0)
| ~ intangibleindividual(X0) ),
inference(cnf_transformation,[status(thm)],[f65391]) ).
fof(f68742,plain,
! [ARG1,ARG2] :
( collection(ARG1)
| ~ genls(ARG1,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f19537]) ).
fof(f68743,plain,
! [ARG1] :
( collection(ARG1)
| ! [ARG2] : ~ genls(ARG1,ARG2) ),
inference(miniscoping,[status(thm)],[f68742]) ).
fof(f68744,plain,
! [X0,X1] :
( collection(X0)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f68743]) ).
fof(f110738,plain,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(cnf_transformation,[status(thm)],[f44218]) ).
fof(f110751,plain,
microtheory(c_wamt_evalinitial_p14),
inference(resolution,[status(thm)],[f52658,f44912]) ).
fof(f110784,plain,
! [X0] :
( individual(X0)
| ~ intangibleindividual(X0) ),
inference(resolution,[status(thm)],[f65392,f57020]) ).
fof(f112089,plain,
collection(c_wamt_evalinitial_p14),
inference(resolution,[status(thm)],[f110738,f68744]) ).
fof(f112129,plain,
! [X0] :
( ~ aspatialinformationstore(X0)
| individual(X0) ),
inference(resolution,[status(thm)],[f110784,f51910]) ).
fof(f112154,plain,
~ individual(c_wamt_evalinitial_p14),
inference(resolution,[status(thm)],[f112089,f49266]) ).
fof(f112168,plain,
! [X0] :
( ~ microtheory(X0)
| individual(X0) ),
inference(resolution,[status(thm)],[f112129,f50695]) ).
fof(f112192,plain,
individual(c_wamt_evalinitial_p14),
inference(resolution,[status(thm)],[f112168,f110751]) ).
fof(f112196,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f112192,f112154]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR045+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.51 % Computer : n016.cluster.edu
% 0.09/0.51 % Model : x86_64 x86_64
% 0.09/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.51 % Memory : 8046.5625MB
% 0.09/0.51 % OS : Linux 6.8.0-71-generic
% 0.09/0.51 % CPULimit : 300
% 0.09/0.51 % WCLimit : 300
% 0.09/0.51 % DateTime : Mon Sep 21 14:37:54 UTC 2026
% 0.09/0.52 % CPUTime :
% 1.00/1.46 % Drodi V4.1.1
% 97.98/13.81 % Refutation found
% 97.98/13.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 97.98/13.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.18/14.17 % Elapsed time: 13.609527 seconds
% 4.18/14.17 % CPU time: 99.528819 seconds
% 4.18/14.17 % Total memory used: 2.015 GB
% 4.18/14.17 % Net memory used: 2.009 GB
%------------------------------------------------------------------------------