%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN708-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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 : Fri Sep 25 03:41:26 PM UTC 2026
% Result : Unsatisfiable 11.92s 2.28s
% Output : CNFRefutation 11.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 73 ( 73 unt; 0 def)
% Number of atoms : 73 ( 72 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 6 con; 0-4 aty)
% Number of variables : 68 ( 0 sgn 68 !; 0 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq2(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f3,negated_conjecture,
p38(c56) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c56_is_p38_1) ).
fof(f4,negated_conjecture,
! [X0] : p10(X0,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_3) ).
fof(f5,plain,
! [X0] : true = p10(X0,X0),
inference(reorient_equations,[],[f4]) ).
fof(f20,negated_conjecture,
p37(f15(c56),c48) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p37_13) ).
fof(f21,plain,
true = p37(f15(c56),c48),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
! [X0] : ifeq2(p38(X0),true,p38(f15(X0)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p38_15) ).
fof(f23,plain,
! [X0] : true = ifeq2(p38(X0),true,p38(f15(X0)),true),
inference(reorient_equations,[],[f22]) ).
fof(f30,negated_conjecture,
! [X0,X1] : ifeq2(p10(X0,X1),true,ifeq2(p38(X0),true,p38(X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p38_19) ).
fof(f31,plain,
! [X0,X1] : true = ifeq2(p10(X0,X1),true,ifeq2(p38(X0),true,p38(X1),true),true),
inference(reorient_equations,[],[f30]) ).
fof(f56,negated_conjecture,
! [X0,X1] : ifeq2(p10(X0,X1),true,p16(f19(X0),f19(X1)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16_32) ).
fof(f57,plain,
! [X0,X1] : true = ifeq2(p10(X0,X1),true,p16(f19(X0),f19(X1)),true),
inference(reorient_equations,[],[f56]) ).
fof(f64,negated_conjecture,
! [X0] : ifeq2(p38(X0),true,p16(f19(f15(X0)),f28(f19(X0))),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16_36) ).
fof(f65,plain,
! [X0] : true = ifeq2(p38(X0),true,p16(f19(f15(X0)),f28(f19(X0))),true),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
! [X2,X0,X1] : ifeq2(p10(X0,X1),true,ifeq2(p10(X0,X2),true,p10(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_37) ).
fof(f67,plain,
! [X2,X0,X1] : true = ifeq2(p10(X0,X1),true,ifeq2(p10(X0,X2),true,p10(X2,X1),true),true),
inference(reorient_equations,[],[f66]) ).
fof(f96,negated_conjecture,
! [X2,X3,X0,X1] : ifeq2(p39(X0,X1),true,ifeq2(p16(X0,X2),true,ifeq2(p16(X1,X3),true,p39(X2,X3),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p39_52) ).
fof(f97,plain,
! [X2,X3,X0,X1] : true = ifeq2(p39(X0,X1),true,ifeq2(p16(X0,X2),true,ifeq2(p16(X1,X3),true,p39(X2,X3),true),true),true),
inference(reorient_equations,[],[f96]) ).
fof(f100,negated_conjecture,
! [X0,X1] : ifeq2(p37(X0,X1),true,ifeq2(p38(X1),true,ifeq2(p38(X0),true,p39(f19(X0),f19(X1)),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p39_54) ).
fof(f101,plain,
! [X0,X1] : true = ifeq2(p37(X0,X1),true,ifeq2(p38(X1),true,ifeq2(p38(X0),true,p39(f19(X0),f19(X1)),true),true),true),
inference(reorient_equations,[],[f100]) ).
fof(f120,negated_conjecture,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f11_is_p38_64) ).
fof(f121,plain,
true = p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
inference(reorient_equations,[],[f120]) ).
fof(f124,negated_conjecture,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_66) ).
fof(f125,plain,
true = p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
inference(reorient_equations,[],[f124]) ).
fof(f166,negated_conjecture,
ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p39_69) ).
fof(f167,plain,
b = ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b),
inference(reorient_equations,[],[f166]) ).
fof(f168,negated_conjecture,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq2(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[],[f2]) ).
tcf(c_137,negated_conjecture,
p38(c56) = true,
inference(cnf_transformation,[],[f3]) ).
tcf(c_138,negated_conjecture,
! [X0: $i] : p10(X0,X0) = true,
inference(cnf_transformation,[],[f5]) ).
tcf(c_146,negated_conjecture,
p37(f15(c56),c48) = true,
inference(cnf_transformation,[],[f21]) ).
tcf(c_147,negated_conjecture,
! [X0: $i] : ifeq2(p38(X0),true,p38(f15(X0)),true) = true,
inference(cnf_transformation,[],[f23]) ).
tcf(c_151,negated_conjecture,
! [X0: $i,X1: $i] : ifeq2(p10(X0,X1),true,ifeq2(p38(X0),true,p38(X1),true),true) = true,
inference(cnf_transformation,[],[f31]) ).
tcf(c_164,negated_conjecture,
! [X0: $i,X1: $i] : ifeq2(p10(X0,X1),true,p16(f19(X0),f19(X1)),true) = true,
inference(cnf_transformation,[],[f57]) ).
tcf(c_168,negated_conjecture,
! [X0: $i] : ifeq2(p38(X0),true,p16(f19(f15(X0)),f28(f19(X0))),true) = true,
inference(cnf_transformation,[],[f65]) ).
tcf(c_169,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : ifeq2(p10(X0,X1),true,ifeq2(p10(X0,X2),true,p10(X2,X1),true),true) = true,
inference(cnf_transformation,[],[f67]) ).
tcf(c_184,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ifeq2(p39(X0,X1),true,ifeq2(p16(X0,X2),true,ifeq2(p16(X1,X3),true,p39(X2,X3),true),true),true) = true,
inference(cnf_transformation,[],[f97]) ).
tcf(c_186,negated_conjecture,
! [X0: $i,X1: $i] : ifeq2(p37(X0,X1),true,ifeq2(p38(X1),true,ifeq2(p38(X0),true,p39(f19(X0),f19(X1)),true),true),true) = true,
inference(cnf_transformation,[],[f101]) ).
tcf(c_196,negated_conjecture,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
inference(cnf_transformation,[],[f121]) ).
tcf(c_198,negated_conjecture,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
inference(cnf_transformation,[],[f125]) ).
tcf(c_219,negated_conjecture,
ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b) = b,
inference(cnf_transformation,[],[f167]) ).
tcf(c_220,negated_conjecture,
a != b,
inference(cnf_transformation,[],[f168]) ).
tcf(c_7381,plain,
ifeq2(true,true,p38(f15(c56)),true) = true,
inference(superposition,[status(thm)],[c_137,c_147]) ).
tcf(c_7389,plain,
ifeq2(true,true,p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true) = true,
inference(superposition,[status(thm)],[c_198,c_164]) ).
tcf(c_7402,plain,
ifeq2(true,true,p16(f19(f15(c56)),f28(f19(c56))),true) = true,
inference(superposition,[status(thm)],[c_137,c_168]) ).
tcf(c_7463,plain,
ifeq2(true,true,ifeq2(p38(c48),true,ifeq2(p38(f15(c56)),true,p39(f19(f15(c56)),f19(c48)),true),true),true) = true,
inference(superposition,[status(thm)],[c_146,c_186]) ).
tcf(c_7532,plain,
! [X0: $i] : ifeq2(p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),X0),true,ifeq2(true,true,p38(X0),true),true) = true,
inference(superposition,[status(thm)],[c_196,c_151]) ).
tcf(c_7548,plain,
! [X0: $i] : ifeq2(p10(c48,X0),true,ifeq2(true,true,p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),X0),true),true) = true,
inference(superposition,[status(thm)],[c_198,c_169]) ).
tcf(c_7590,plain,
p38(f15(c56)) = true,
inference(demodulation,[status(thm)],[c_7381,c_135]) ).
tcf(c_7592,plain,
p16(f19(f15(c56)),f28(f19(c56))) = true,
inference(demodulation,[status(thm)],[c_7402,c_135]) ).
tcf(c_7634,plain,
ifeq2(p38(c48),true,ifeq2(p38(f15(c56)),true,p39(f19(f15(c56)),f19(c48)),true),true) = true,
inference(demodulation,[status(thm)],[c_7463,c_135]) ).
tcf(c_7641,plain,
p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(demodulation,[status(thm)],[c_7389,c_135]) ).
tcf(c_7654,plain,
! [X0: $i] : ifeq2(p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),X0),true,p38(X0),true) = true,
inference(demodulation,[status(thm)],[c_7532,c_135]) ).
tcf(c_7655,plain,
! [X0: $i] : ifeq2(p10(c48,X0),true,p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),X0),true) = true,
inference(demodulation,[status(thm)],[c_7548,c_135]) ).
tcf(c_8003,plain,
ifeq2(true,true,p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48),true) = true,
inference(superposition,[status(thm)],[c_138,c_7655]) ).
tcf(c_8106,plain,
p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48) = true,
inference(demodulation,[status(thm)],[c_8003,c_135]) ).
tcf(c_8427,plain,
ifeq2(true,true,p38(c48),true) = true,
inference(superposition,[status(thm)],[c_8106,c_7654]) ).
tcf(c_8610,plain,
p38(c48) = true,
inference(demodulation,[status(thm)],[c_8427,c_135]) ).
tcf(c_8816,plain,
ifeq2(true,true,ifeq2(p38(f15(c56)),true,p39(f19(f15(c56)),f19(c48)),true),true) = true,
inference(demodulation,[status(thm)],[c_7634,c_8610]) ).
tcf(c_8818,plain,
ifeq2(p38(f15(c56)),true,p39(f19(f15(c56)),f19(c48)),true) = true,
inference(demodulation,[status(thm)],[c_8816,c_135]) ).
tcf(c_8819,plain,
ifeq2(true,true,p39(f19(f15(c56)),f19(c48)),true) = true,
inference(light_normalisation,[status(thm)],[c_8818,c_7590]) ).
tcf(c_8820,plain,
p39(f19(f15(c56)),f19(c48)) = true,
inference(demodulation,[status(thm)],[c_8819,c_135]) ).
tcf(c_9115,plain,
! [X0: $i,X1: $i] : ifeq2(p39(f19(f15(c56)),X0),true,ifeq2(true,true,ifeq2(p16(X0,X1),true,p39(f28(f19(c56)),X1),true),true),true) = true,
inference(superposition,[status(thm)],[c_7592,c_184]) ).
tcf(c_9250,plain,
! [X0: $i,X1: $i] : ifeq2(p39(f19(f15(c56)),X0),true,ifeq2(p16(X0,X1),true,p39(f28(f19(c56)),X1),true),true) = true,
inference(demodulation,[status(thm)],[c_9115,c_135]) ).
tcf(c_9552,plain,
ifeq2(p39(f19(f15(c56)),f19(c48)),true,ifeq2(true,true,p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true),true) = true,
inference(superposition,[status(thm)],[c_7641,c_9250]) ).
tcf(c_9881,plain,
ifeq2(p39(f19(f15(c56)),f19(c48)),true,p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true) = true,
inference(demodulation,[status(thm)],[c_9552,c_135]) ).
tcf(c_9882,plain,
ifeq2(true,true,p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true) = true,
inference(light_normalisation,[status(thm)],[c_9881,c_8820]) ).
tcf(c_9883,plain,
p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(demodulation,[status(thm)],[c_9882,c_135]) ).
tcf(c_9907,plain,
ifeq(true,true,a,b) = b,
inference(demodulation,[status(thm)],[c_219,c_9883]) ).
tcf(c_9908,plain,
a = b,
inference(demodulation,[status(thm)],[c_9907,c_136]) ).
tcf(c_9909,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_9908,c_220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN708-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 02:10:49 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running UEQ theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 11.92/2.28 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 11.92/2.28 % SZS status Started for theBenchmark.p
% 11.92/2.28 % SZS status Unsatisfiable for theBenchmark.p
% 11.92/2.28
% 11.92/2.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 11.92/2.28
% 11.92/2.28 % ------ iProver source info
% 11.92/2.28
% 11.92/2.28 % git: date: 2026-07-19 20:42:38 +0200
% 11.92/2.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 11.92/2.28 % git: non_committed_changes: false
% 11.92/2.28
% 11.92/2.28 % ------ Parsing...% successful
% 11.92/2.28
% 11.92/2.28
% 11.92/2.28 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 11.92/2.28 % ------ Proving...
% 11.92/2.28 % ------ Problem Properties
% 11.92/2.28
% 11.92/2.28 %
% 11.92/2.28 % clauses 86
% 11.92/2.28 % conjectures 84
% 11.92/2.28 % EPR 1
% 11.92/2.28 % Horn 86
% 11.92/2.28 % unary 86
% 11.92/2.28 % binary 0
% 11.92/2.28 % lits 86
% 11.92/2.28 % lits eq 86
% 11.92/2.28 % fd_pure 0
% 11.92/2.28 % fd_pseudo 0
% 11.92/2.28 % fd_cond 0
% 11.92/2.28 % fd_pseudo_cond 0
% 11.92/2.28 % AC symbols 0
% 11.92/2.28
% 11.92/2.28 % ------ Input Options Time Limit: Unbounded
% 11.92/2.28
% 11.92/2.28
% 11.92/2.28 % ------
% 11.92/2.28 % Current options:
% 11.92/2.28 % ------
% 11.92/2.28
% 11.92/2.28
% 11.92/2.28 %
% 11.92/2.28
% 11.92/2.28 % ------ Proving...
% 11.92/2.28 %
% 11.92/2.28
% 11.92/2.28 % SZS status Unsatisfiable for theBenchmark.p
% 11.92/2.28
% 11.92/2.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 11.92/2.28
% 11.92/2.28
%------------------------------------------------------------------------------