%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR044-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:48 AM UTC 2026
% Result : Unsatisfiable 0.14s 5.50s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 14
% Syntax : Number of formulae : 54 ( 54 unt; 0 def)
% Number of atoms : 54 ( 53 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 : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 10 con; 0-4 aty)
% Number of variables : 34 ( 2 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax2_2981,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq4(relationallexists(VAR_0,VAR_1,VAR_2),true,ifeq4(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',ax2_2981) ).
cnf(c_4,plain,
ifeq4(relationallexists(A,B,C),true,ifeq4(isa(D,B),true,isa(f_relationallexistsfn(D,A,B,C),C),true),true) = true,
inference(clausify,[status(thm)],[ax2_2981]) ).
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq4(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_27,plain,
ifeq4(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(ifeq_axiom_002,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_002) ).
cnf(c_28,plain,
ifeq2(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_002]) ).
fof(ax2_19,axiom,
executionbyfiringsquad(c_tptpexecutionbyfiringsquad_90) = true,
file('theBenchmark.p',ax2_19) ).
cnf(c_29,plain,
executionbyfiringsquad(c_tptpexecutionbyfiringsquad_90) = true,
inference(clausify,[status(thm)],[ax2_19]) ).
fof(ax2_142,axiom,
genlmt(c_tptp_member3633_mt,c_tptp_spindleheadmt) = true,
file('theBenchmark.p',ax2_142) ).
cnf(c_30,plain,
genlmt(c_tptp_member3633_mt,c_tptp_spindleheadmt) = true,
inference(clausify,[status(thm)],[ax2_142]) ).
fof(ax2_2495,axiom,
! [VAR_0] : ifeq4(executionbyfiringsquad(VAR_0),true,ifeq4(mtvisible(c_cyclistsmt),true,tptp_9_720(VAR_0,f_relationallexistsfn(VAR_0,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),true),true) = true,
file('theBenchmark.p',ax2_2495) ).
cnf(c_35,plain,
ifeq4(executionbyfiringsquad(A),true,ifeq4(mtvisible(c_cyclistsmt),true,tptp_9_720(A,f_relationallexistsfn(A,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),true),true) = true,
inference(clausify,[status(thm)],[ax2_2495]) ).
fof(ax2_2496,axiom,
ifeq4(mtvisible(c_cyclistsmt),true,relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),true) = true,
file('theBenchmark.p',ax2_2496) ).
cnf(c_36,plain,
ifeq4(mtvisible(c_cyclistsmt),true,relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),true) = true,
inference(clausify,[status(thm)],[ax2_2496]) ).
fof(ax2_4288,axiom,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt) = true,
file('theBenchmark.p',ax2_4288) ).
cnf(c_46,plain,
genlmt(c_tptp_spindleheadmt,c_cyclistsmt) = true,
inference(clausify,[status(thm)],[ax2_4288]) ).
fof(ax2_5730,axiom,
! [VAR_0] : ifeq4(isa(VAR_0,c_tptpcol_16_29490),true,tptpcol_16_29490(VAR_0),true) = true,
file('theBenchmark.p',ax2_5730) ).
cnf(c_48,plain,
ifeq4(isa(A,c_tptpcol_16_29490),true,tptpcol_16_29490(A),true) = true,
inference(clausify,[status(thm)],[ax2_5730]) ).
fof(ax2_7920,axiom,
! [VAR_0] : ifeq4(executionbyfiringsquad(VAR_0),true,isa(VAR_0,c_executionbyfiringsquad),true) = true,
file('theBenchmark.p',ax2_7920) ).
cnf(c_55,plain,
ifeq4(executionbyfiringsquad(A),true,isa(A,c_executionbyfiringsquad),true) = true,
inference(clausify,[status(thm)],[ax2_7920]) ).
fof(ax2_7997,axiom,
! [VAR_0,VAR_1] : ifeq4(genlmt(VAR_0,VAR_1),true,ifeq4(mtvisible(VAR_0),true,mtvisible(VAR_1),true),true) = true,
file('theBenchmark.p',ax2_7997) ).
cnf(c_65,plain,
ifeq4(genlmt(A,B),true,ifeq4(mtvisible(A),true,mtvisible(B),true),true) = true,
inference(clausify,[status(thm)],[ax2_7997]) ).
fof(query144,axiom,
mtvisible(c_tptp_member3633_mt) = true,
file('theBenchmark.p',query144) ).
cnf(c_67,plain,
mtvisible(c_tptp_member3633_mt) = true,
inference(clausify,[status(thm)],[query144]) ).
fof(query144_1,axiom,
! [VAR_0] : ifeq2(tuple2(tptp_9_720(c_tptpexecutionbyfiringsquad_90,VAR_0),tptpcol_16_29490(VAR_0)),tuple2(true,true),a,b) = b,
file('theBenchmark.p',query144_1) ).
cnf(c_72,plain,
ifeq2(tuple2(tptp_9_720(c_tptpexecutionbyfiringsquad_90,A),tptpcol_16_29490(A)),tuple2(true,true),a,b) = b,
inference(clausify,[status(thm)],[query144_1]) ).
fof(goal,axiom,
a != b,
file('theBenchmark.p',goal) ).
cnf(c_73,plain,
a != b,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_295,plain,
ifeq4(true,true,ifeq4(mtvisible(c_tptp_member3633_mt),true,mtvisible(c_tptp_spindleheadmt),true),true) = true,
inference(paramod,[status(thm)],[c_30,c_65]) ).
cnf(c_296,plain,
ifeq4(true,true,ifeq4(true,true,mtvisible(c_tptp_spindleheadmt),true),true) = true,
inference(paramod,[status(thm)],[c_67,c_295]) ).
cnf(c_297,plain,
ifeq4(true,true,mtvisible(c_tptp_spindleheadmt),true) = true,
inference(paramod,[status(thm)],[c_27,c_296]) ).
cnf(c_78,plain,
mtvisible(c_tptp_spindleheadmt) = true,
inference(paramod,[status(thm)],[c_27,c_297]) ).
cnf(c_298,plain,
ifeq4(true,true,ifeq4(mtvisible(c_cyclistsmt),true,tptp_9_720(c_tptpexecutionbyfiringsquad_90,f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),true),true) = true,
inference(paramod,[status(thm)],[c_29,c_35]) ).
cnf(c_83,plain,
ifeq4(mtvisible(c_cyclistsmt),true,tptp_9_720(c_tptpexecutionbyfiringsquad_90,f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),true) = true,
inference(paramod,[status(thm)],[c_27,c_298]) ).
cnf(c_299,plain,
ifeq4(true,true,ifeq4(mtvisible(c_tptp_spindleheadmt),true,mtvisible(c_cyclistsmt),true),true) = true,
inference(paramod,[status(thm)],[c_46,c_65]) ).
cnf(c_300,plain,
ifeq4(true,true,ifeq4(true,true,mtvisible(c_cyclistsmt),true),true) = true,
inference(paramod,[status(thm)],[c_78,c_299]) ).
cnf(c_301,plain,
ifeq4(true,true,mtvisible(c_cyclistsmt),true) = true,
inference(paramod,[status(thm)],[c_27,c_300]) ).
cnf(c_100,plain,
mtvisible(c_cyclistsmt) = true,
inference(paramod,[status(thm)],[c_27,c_301]) ).
cnf(c_302,plain,
ifeq4(true,true,tptp_9_720(c_tptpexecutionbyfiringsquad_90,f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),true) = true,
inference(paramod,[status(thm)],[c_100,c_83]) ).
cnf(c_101,plain,
tptp_9_720(c_tptpexecutionbyfiringsquad_90,f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)) = true,
inference(paramod,[status(thm)],[c_27,c_302]) ).
cnf(c_303,plain,
ifeq4(true,true,relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),true) = true,
inference(paramod,[status(thm)],[c_100,c_36]) ).
cnf(c_102,plain,
relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490) = true,
inference(paramod,[status(thm)],[c_27,c_303]) ).
cnf(c_304,plain,
ifeq4(true,true,ifeq4(isa(A,c_executionbyfiringsquad),true,isa(f_relationallexistsfn(A,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),c_tptpcol_16_29490),true),true) = true,
inference(paramod,[status(thm)],[c_102,c_4]) ).
cnf(c_115,plain,
ifeq4(isa(A,c_executionbyfiringsquad),true,isa(f_relationallexistsfn(A,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),c_tptpcol_16_29490),true) = true,
inference(paramod,[status(thm)],[c_27,c_304]) ).
cnf(c_198,plain,
ifeq2(tuple2(true,tptpcol_16_29490(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490))),tuple2(true,true),a,b) = b,
inference(paramod,[status(thm)],[c_101,c_72]) ).
cnf(c_305,plain,
ifeq4(true,true,isa(c_tptpexecutionbyfiringsquad_90,c_executionbyfiringsquad),true) = true,
inference(paramod,[status(thm)],[c_29,c_55]) ).
cnf(c_199,plain,
isa(c_tptpexecutionbyfiringsquad_90,c_executionbyfiringsquad) = true,
inference(paramod,[status(thm)],[c_27,c_305]) ).
cnf(c_306,plain,
ifeq4(true,true,isa(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),c_tptpcol_16_29490),true) = true,
inference(paramod,[status(thm)],[c_199,c_115]) ).
cnf(c_288,plain,
isa(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),c_tptpcol_16_29490) = true,
inference(paramod,[status(thm)],[c_27,c_306]) ).
cnf(c_307,plain,
ifeq4(true,true,tptpcol_16_29490(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),true) = true,
inference(paramod,[status(thm)],[c_288,c_48]) ).
cnf(c_292,plain,
tptpcol_16_29490(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)) = true,
inference(paramod,[status(thm)],[c_27,c_307]) ).
cnf(c_308,plain,
ifeq2(tuple2(true,true),tuple2(true,true),a,b) = b,
inference(paramod,[status(thm)],[c_292,c_198]) ).
cnf(c_293,plain,
a = b,
inference(paramod,[status(thm)],[c_28,c_308]) ).
cnf(c_294,plain,
$false,
inference(resolve,[status(thm)],[c_293,c_73]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR044-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n019.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 : Sun Sep 27 00:13:11 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.38 % Process 2540186 was started by sandbox on n019,
% 0.09/5.38 % Sun Sep 27 00:13:11 2026
% 0.09/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/5.50
% 0.14/5.50 % SInE (scan): 65 to sos (tol 1.5x), 8 to usable (tol 2.0x), 7939 zapped, of 8012 axioms (depth 3).
% 0.14/5.50
% 0.14/5.50 % From the command line: assign(max_seconds, 300).
% 0.14/5.50
% 0.14/5.50 % SZS status Unsatisfiable for theBenchmark
% 0.14/5.50
% 0.14/5.50 % Proof 1 at 0.04 (+ 0.02) seconds.
% 0.14/5.50 % Length of proof is 26.
% 0.14/5.50 % Level of proof is 8.
% 0.14/5.50 % Maximum clause weight is 119.000.
% 0.14/5.50 % Given clauses 164.
% 0.14/5.50
% 0.14/5.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------