%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR027-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:06:35 AM UTC 2026
% Result : Unsatisfiable 0.09s 0.48s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 12
% Syntax : Number of formulae : 44 ( 44 unt; 0 def)
% Number of atoms : 44 ( 43 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-4 aty)
% Number of variables : 34 ( 2 sgn 15 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq3(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq3(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(ifeq_axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c_2,plain,
ifeq2(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_001]) ).
fof(just1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq3(relationallexists(VAR_0,VAR_1,VAR_2),true,ifeq3(isa(VAR_3,VAR_1),true,isa(f_relationallexistsfn(VAR_3,VAR_0,VAR_1,VAR_2),VAR_2),true),true) = true,
file('theBenchmark.p',just1) ).
cnf(c_4,plain,
ifeq3(relationallexists(A,B,C),true,ifeq3(isa(D,B),true,isa(f_relationallexistsfn(D,A,B,C),C),true),true) = true,
inference(clausify,[status(thm)],[just1]) ).
fof(just9,axiom,
genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt) = true,
file('theBenchmark.p',just9) ).
cnf(c_12,plain,
genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt) = true,
inference(clausify,[status(thm)],[just9]) ).
fof(just12,axiom,
! [VAR_0] : ifeq3(mtvisible(c_tptp_member2610_mt),true,ifeq3(isa(VAR_0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),true,tptp_8_875(VAR_0,f_relationallexistsfn(VAR_0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)),true),true) = true,
file('theBenchmark.p',just12) ).
cnf(c_15,plain,
ifeq3(mtvisible(c_tptp_member2610_mt),true,ifeq3(isa(A,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),true,tptp_8_875(A,f_relationallexistsfn(A,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)),true),true) = true,
inference(clausify,[status(thm)],[just12]) ).
fof(just13,axiom,
ifeq3(mtvisible(c_tptp_member2610_mt),true,relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868),true) = true,
file('theBenchmark.p',just13) ).
cnf(c_16,plain,
ifeq3(mtvisible(c_tptp_member2610_mt),true,relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868),true) = true,
inference(clausify,[status(thm)],[just13]) ).
fof(just14,axiom,
isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) = true,
file('theBenchmark.p',just14) ).
cnf(c_17,plain,
isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) = true,
inference(clausify,[status(thm)],[just14]) ).
fof(just34,axiom,
! [VAR_0] : ifeq3(isa(VAR_0,c_tptpcol_16_31868),true,tptpcol_16_31868(VAR_0),true) = true,
file('theBenchmark.p',just34) ).
cnf(c_36,plain,
ifeq3(isa(A,c_tptpcol_16_31868),true,tptpcol_16_31868(A),true) = true,
inference(clausify,[status(thm)],[just34]) ).
fof(just63,axiom,
! [VAR_0,VAR_1] : ifeq3(genlmt(VAR_0,VAR_1),true,ifeq3(mtvisible(VAR_0),true,mtvisible(VAR_1),true),true) = true,
file('theBenchmark.p',just63) ).
cnf(c_65,plain,
ifeq3(genlmt(A,B),true,ifeq3(mtvisible(A),true,mtvisible(B),true),true) = true,
inference(clausify,[status(thm)],[just63]) ).
fof(query27,axiom,
mtvisible(c_tptp_spindlecollectormt) = true,
file('theBenchmark.p',query27) ).
cnf(c_82,plain,
mtvisible(c_tptp_spindlecollectormt) = true,
inference(clausify,[status(thm)],[query27]) ).
fof(query27_1,axiom,
! [VAR_0] : ifeq2(tuple2(tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,VAR_0),tptpcol_16_31868(VAR_0)),tuple2(true,true),a,b) = b,
file('theBenchmark.p',query27_1) ).
cnf(c_84,plain,
ifeq2(tuple2(tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,A),tptpcol_16_31868(A)),tuple2(true,true),a,b) = b,
inference(clausify,[status(thm)],[query27_1]) ).
fof(goal,axiom,
a != b,
file('theBenchmark.p',goal) ).
cnf(c_85,plain,
a != b,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_322,plain,
ifeq3(relationallexists(A,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),B),true,ifeq3(true,true,isa(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,A,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),B),B),true),true) = true,
inference(paramod,[status(thm)],[c_17,c_4]) ).
cnf(c_86,plain,
ifeq3(relationallexists(A,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),B),true,isa(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,A,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),B),B),true) = true,
inference(paramod,[status(thm)],[c_1,c_322]) ).
cnf(c_323,plain,
ifeq3(mtvisible(c_tptp_member2610_mt),true,ifeq3(true,true,tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)),true),true) = true,
inference(paramod,[status(thm)],[c_17,c_15]) ).
cnf(c_87,plain,
ifeq3(mtvisible(c_tptp_member2610_mt),true,tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)),true) = true,
inference(paramod,[status(thm)],[c_1,c_323]) ).
cnf(c_324,plain,
ifeq3(true,true,ifeq3(mtvisible(c_tptp_spindlecollectormt),true,mtvisible(c_tptp_member2610_mt),true),true) = true,
inference(paramod,[status(thm)],[c_12,c_65]) ).
cnf(c_325,plain,
ifeq3(true,true,ifeq3(true,true,mtvisible(c_tptp_member2610_mt),true),true) = true,
inference(paramod,[status(thm)],[c_82,c_324]) ).
cnf(c_326,plain,
ifeq3(true,true,mtvisible(c_tptp_member2610_mt),true) = true,
inference(paramod,[status(thm)],[c_1,c_325]) ).
cnf(c_104,plain,
mtvisible(c_tptp_member2610_mt) = true,
inference(paramod,[status(thm)],[c_1,c_326]) ).
cnf(c_327,plain,
ifeq3(true,true,tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)),true) = true,
inference(paramod,[status(thm)],[c_104,c_87]) ).
cnf(c_109,plain,
tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)) = true,
inference(paramod,[status(thm)],[c_1,c_327]) ).
cnf(c_328,plain,
ifeq3(true,true,relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868),true) = true,
inference(paramod,[status(thm)],[c_104,c_16]) ).
cnf(c_110,plain,
relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868) = true,
inference(paramod,[status(thm)],[c_1,c_328]) ).
cnf(c_224,plain,
ifeq2(tuple2(true,tptpcol_16_31868(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))),tuple2(true,true),a,b) = b,
inference(paramod,[status(thm)],[c_109,c_84]) ).
cnf(c_329,plain,
ifeq3(true,true,isa(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868),c_tptpcol_16_31868),true) = true,
inference(paramod,[status(thm)],[c_110,c_86]) ).
cnf(c_228,plain,
isa(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868),c_tptpcol_16_31868) = true,
inference(paramod,[status(thm)],[c_1,c_329]) ).
cnf(c_330,plain,
ifeq3(true,true,tptpcol_16_31868(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)),true) = true,
inference(paramod,[status(thm)],[c_228,c_36]) ).
cnf(c_315,plain,
tptpcol_16_31868(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)) = true,
inference(paramod,[status(thm)],[c_1,c_330]) ).
cnf(c_331,plain,
ifeq2(tuple2(true,true),tuple2(true,true),a,b) = b,
inference(paramod,[status(thm)],[c_315,c_224]) ).
cnf(c_320,plain,
a = b,
inference(paramod,[status(thm)],[c_2,c_331]) ).
cnf(c_321,plain,
$false,
inference(resolve,[status(thm)],[c_320,c_85]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR027-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.40 % Computer : n013.cluster.edu
% 0.09/0.40 % Model : x86_64 x86_64
% 0.09/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.40 % Memory : 8046.5625MB
% 0.09/0.40 % OS : Linux 6.8.0-71-generic
% 0.09/0.40 % CPULimit : 300
% 0.09/0.40 % WCLimit : 300
% 0.09/0.40 % DateTime : Sat Sep 26 23:56:51 UTC 2026
% 0.09/0.40 % CPUTime :
% 0.09/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.41 % Process 3847085 was started by sandbox on n013,
% 0.09/0.41 % Sat Sep 26 23:56:51 2026
% 0.09/0.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.41
% 0.09/0.41 % From the command line: assign(max_seconds, 300).
% 0.09/0.48
% 0.09/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.09/0.48
% 0.09/0.48 % Proof 1 at 0.05 (+ 0.01) seconds.
% 0.09/0.48 % Length of proof is 22.
% 0.09/0.48 % Level of proof is 6.
% 0.09/0.48 % Maximum clause weight is 56.000.
% 0.09/0.48 % Given clauses 240.
% 0.09/0.48
% 0.09/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------