%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT393-2 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n004.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 01:59:47 PM UTC 2026
% Result : Unsatisfiable 249.14s 37.30s
% Output : CNFRefutation 249.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 8
% Syntax : Number of formulae : 171 ( 171 unt; 6 def)
% Number of atoms : 726 ( 170 equ)
% Maximal formula atoms : 1 ( 4 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 7 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 196 ( 0 sgn 196 !; 0 ?; 192 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos) ).
fof(f2,negated_conjecture,
f(x0,f(f(x1,x2),f(x1,x2))) != f(x1,f(f(x0,x2),f(x0,x2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
f(x0,f(f(x1,x2),f(x1,x2))) != f(x1,f(f(x0,x2),f(x0,x2))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,definition,
iPr_def_10 = f(x1,x2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_62,definition,
iPr_def_11 = f(iPr_def_10,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_63,definition,
iPr_def_12 = f(x0,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_64,definition,
iPr_def_13 = f(x0,x2),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_65,definition,
iPr_def_14 = f(iPr_def_13,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_66,definition,
iPr_def_15 = f(x1,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_67,negated_conjecture,
iPr_def_12 != iPr_def_15,
inference(demodulation,[status(thm)],[c_52,c_64,c_65,c_66,c_61,c_62,c_63]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))) = X1,
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_10,f(x2,X0)),X1),f(x2,f(f(x2,f(f(x1,x1),x1)),X0))) = x2,
inference(superposition,[status(thm)],[c_61,c_68]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_13,f(x2,X0)),X1),f(x2,f(f(x2,f(f(x0,x0),x0)),X0))) = x2,
inference(superposition,[status(thm)],[c_64,c_68]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_11,f(iPr_def_10,X0)),X1),f(iPr_def_10,f(f(iPr_def_10,f(iPr_def_11,iPr_def_10)),X0))) = iPr_def_10,
inference(superposition,[status(thm)],[c_62,c_68]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_12,f(iPr_def_11,X0)),X1),f(iPr_def_11,f(f(iPr_def_11,f(f(x0,x0),x0)),X0))) = iPr_def_11,
inference(superposition,[status(thm)],[c_63,c_68]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_14,f(iPr_def_13,X0)),X1),f(iPr_def_13,f(f(iPr_def_13,f(iPr_def_14,iPr_def_13)),X0))) = iPr_def_13,
inference(superposition,[status(thm)],[c_65,c_68]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_15,f(iPr_def_14,X0)),X1),f(iPr_def_14,f(f(iPr_def_14,f(f(x1,x1),x1)),X0))) = iPr_def_14,
inference(superposition,[status(thm)],[c_66,c_68]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,x1),iPr_def_10),X1),f(x1,f(f(x1,f(f(X0,X0),X0)),x2))) = x1,
inference(superposition,[status(thm)],[c_61,c_68]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,x0),iPr_def_13),X1),f(x0,f(f(x0,f(f(X0,X0),X0)),x2))) = x0,
inference(superposition,[status(thm)],[c_64,c_68]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,x0),iPr_def_12),X1),f(x0,f(f(x0,f(f(X0,X0),X0)),iPr_def_11))) = x0,
inference(superposition,[status(thm)],[c_63,c_68]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,x1),iPr_def_15),X1),f(x1,f(f(x1,f(f(X0,X0),X0)),iPr_def_14))) = x1,
inference(superposition,[status(thm)],[c_66,c_68]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(iPr_def_10,X0),f(X0,X1)),X2),f(X0,f(f(X0,f(iPr_def_11,iPr_def_10)),X1))) = X0,
inference(superposition,[status(thm)],[c_62,c_68]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(iPr_def_13,X0),f(X0,X1)),X2),f(X0,f(f(X0,f(iPr_def_14,iPr_def_13)),X1))) = X0,
inference(superposition,[status(thm)],[c_65,c_68]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(X0,X1),f(X0,f(f(X0,f(f(f(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3))),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(f(X2,X2),X2)),X3)))) = X0,
inference(superposition,[status(thm)],[c_68,c_68]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(X0,f(f(X0,X1),f(f(f(X0,X1),f(f(f(X2,X0),f(X2,X0)),f(X2,X0))),X3))) = f(X0,X1),
inference(superposition,[status(thm)],[c_68,c_68]) ).
tcf(c_147,plain,
! [X0: $i] : f(f(f(iPr_def_11,iPr_def_11),X0),f(iPr_def_10,f(f(iPr_def_10,f(iPr_def_11,iPr_def_10)),iPr_def_10))) = iPr_def_10,
inference(superposition,[status(thm)],[c_62,c_109]) ).
tcf(c_162,plain,
! [X0: $i] : f(iPr_def_10,f(iPr_def_11,f(f(iPr_def_11,f(f(iPr_def_11,iPr_def_11),iPr_def_11)),X0))) = iPr_def_11,
inference(superposition,[status(thm)],[c_147,c_68]) ).
tcf(c_176,plain,
! [X0: $i] : f(f(f(iPr_def_14,iPr_def_14),X0),f(iPr_def_13,f(f(iPr_def_13,f(iPr_def_14,iPr_def_13)),iPr_def_13))) = iPr_def_13,
inference(superposition,[status(thm)],[c_65,c_111]) ).
tcf(c_191,plain,
! [X0: $i] : f(iPr_def_13,f(iPr_def_14,f(f(iPr_def_14,f(f(iPr_def_14,iPr_def_14),iPr_def_14)),X0))) = iPr_def_14,
inference(superposition,[status(thm)],[c_176,c_68]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i] : f(x2,f(f(x2,X0),f(f(f(x2,X0),f(f(iPr_def_10,iPr_def_10),iPr_def_10)),X1))) = f(x2,X0),
inference(superposition,[status(thm)],[c_107,c_68]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i] : f(x2,f(f(x2,X0),f(f(f(x2,X0),f(iPr_def_11,iPr_def_10)),X1))) = f(x2,X0),
inference(demodulation,[status(thm)],[c_208,c_62]) ).
tcf(c_291,plain,
! [X0: $i,X1: $i] : f(iPr_def_11,f(f(iPr_def_11,X0),f(f(f(iPr_def_11,X0),f(f(iPr_def_12,iPr_def_12),iPr_def_12)),X1))) = f(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_110,c_68]) ).
tcf(c_301,plain,
! [X0: $i,X1: $i] : f(iPr_def_14,f(f(iPr_def_14,X0),f(f(f(iPr_def_14,X0),f(f(iPr_def_15,iPr_def_15),iPr_def_15)),X1))) = f(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_112,c_68]) ).
tcf(c_902,plain,
f(iPr_def_10,f(iPr_def_11,f(f(iPr_def_11,iPr_def_11),iPr_def_11))) = iPr_def_11,
inference(superposition,[status(thm)],[c_291,c_162]) ).
tcf(c_929,plain,
! [X0: $i] : f(f(f(f(iPr_def_13,iPr_def_10),iPr_def_11),X0),f(iPr_def_10,f(f(iPr_def_10,f(iPr_def_14,iPr_def_13)),f(iPr_def_11,f(f(iPr_def_11,iPr_def_11),iPr_def_11))))) = iPr_def_10,
inference(superposition,[status(thm)],[c_902,c_122]) ).
tcf(c_972,plain,
f(iPr_def_13,f(iPr_def_14,f(f(iPr_def_14,iPr_def_14),iPr_def_14))) = iPr_def_14,
inference(superposition,[status(thm)],[c_301,c_191]) ).
tcf(c_995,plain,
! [X0: $i] : f(f(f(f(iPr_def_10,iPr_def_13),iPr_def_14),X0),f(iPr_def_13,f(f(iPr_def_13,f(iPr_def_11,iPr_def_10)),f(iPr_def_14,f(f(iPr_def_14,iPr_def_14),iPr_def_14))))) = iPr_def_13,
inference(superposition,[status(thm)],[c_972,c_121]) ).
tcf(c_1400,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(X0,X1),f(f(f(X0,X1),f(X1,X2)),X1)) = f(f(X0,X1),f(X1,X2)),
inference(superposition,[status(thm)],[c_68,c_126]) ).
tcf(c_1411,plain,
! [X0: $i] : f(f(X0,x0),f(f(f(X0,x0),iPr_def_12),x0)) = f(f(X0,x0),iPr_def_12),
inference(superposition,[status(thm)],[c_117,c_126]) ).
tcf(c_1413,plain,
! [X0: $i] : f(f(X0,x1),f(f(f(X0,x1),iPr_def_15),x1)) = f(f(X0,x1),iPr_def_15),
inference(superposition,[status(thm)],[c_119,c_126]) ).
tcf(c_1794,plain,
! [X0: $i] : f(iPr_def_11,f(f(iPr_def_11,X0),f(f(iPr_def_12,iPr_def_12),iPr_def_12))) = f(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_126,c_291]) ).
tcf(c_1796,plain,
! [X0: $i] : f(iPr_def_14,f(f(iPr_def_14,X0),f(f(iPr_def_15,iPr_def_15),iPr_def_15))) = f(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_126,c_301]) ).
tcf(c_2387,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,X1),f(X1,X2)),X1),f(X1,X1)) = X1,
inference(superposition,[status(thm)],[c_68,c_1400]) ).
tcf(c_2832,plain,
f(f(iPr_def_10,iPr_def_10),f(iPr_def_10,iPr_def_10)) = iPr_def_10,
inference(superposition,[status(thm)],[c_929,c_2387]) ).
tcf(c_2837,plain,
f(f(iPr_def_13,iPr_def_13),f(iPr_def_13,iPr_def_13)) = iPr_def_13,
inference(superposition,[status(thm)],[c_995,c_2387]) ).
tcf(c_3025,plain,
! [X0: $i] : f(f(X0,X0),f(X0,X0)) = X0,
inference(superposition,[status(thm)],[c_2387,c_2387]) ).
tcf(c_3031,plain,
f(iPr_def_14,iPr_def_14) = iPr_def_13,
inference(demodulation,[status(thm)],[c_2837,c_65]) ).
tcf(c_3032,plain,
f(iPr_def_11,iPr_def_11) = iPr_def_10,
inference(demodulation,[status(thm)],[c_2832,c_62]) ).
tcf(c_6132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(X0,f(f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))),X3)),f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2)))),f(f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))),f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))))) = f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))),
inference(superposition,[status(thm)],[c_125,c_2387]) ).
tcf(c_6145,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(X0,X1),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))) = X1,
inference(superposition,[status(thm)],[c_125,c_68]) ).
tcf(c_6159,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X0,X1),f(X0,X1))) = f(X0,X1),
inference(superposition,[status(thm)],[c_125,c_126]) ).
tcf(c_6257,plain,
! [X0: $i,X1: $i,X2: $i] : f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))) = f(X0,X0),
inference(demodulation,[status(thm)],[c_6132,c_125]) ).
tcf(c_6258,plain,
! [X0: $i,X1: $i] : f(f(X0,X1),f(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_125,c_6257]) ).
tcf(c_7604,plain,
f(iPr_def_13,iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_3031,c_3025]) ).
tcf(c_7912,plain,
! [X0: $i,X1: $i] : f(f(f(X0,X0),X1),X0) = f(X0,X0),
inference(superposition,[status(thm)],[c_6258,c_6258]) ).
tcf(c_7944,plain,
! [X0: $i] : f(f(f(iPr_def_12,f(iPr_def_11,f(iPr_def_11,iPr_def_11))),X0),f(iPr_def_11,iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_6258,c_110]) ).
tcf(c_7948,plain,
! [X0: $i] : f(f(f(iPr_def_15,f(iPr_def_14,f(iPr_def_14,iPr_def_14))),X0),f(iPr_def_14,iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_6258,c_112]) ).
tcf(c_8001,plain,
! [X0: $i] : f(f(f(iPr_def_15,f(iPr_def_14,iPr_def_13)),X0),iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_7948,c_3031]) ).
tcf(c_8003,plain,
! [X0: $i] : f(f(f(iPr_def_12,f(iPr_def_11,iPr_def_10)),X0),iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7944,c_3032]) ).
tcf(c_9312,plain,
! [X0: $i,X1: $i] : f(f(X0,X0),f(X0,X0)) = f(f(X0,X0),f(X0,X1)),
inference(superposition,[status(thm)],[c_7912,c_1400]) ).
tcf(c_9389,plain,
f(f(x0,x0),f(x0,x0)) = f(f(x0,x0),iPr_def_12),
inference(superposition,[status(thm)],[c_7912,c_1411]) ).
tcf(c_9392,plain,
f(f(x1,x1),f(x1,x1)) = f(f(x1,x1),iPr_def_15),
inference(superposition,[status(thm)],[c_7912,c_1413]) ).
tcf(c_9404,plain,
f(f(x1,x1),iPr_def_15) = x1,
inference(demodulation,[status(thm)],[c_9392,c_6258]) ).
tcf(c_9405,plain,
f(f(x0,x0),iPr_def_12) = x0,
inference(demodulation,[status(thm)],[c_9389,c_6258]) ).
tcf(c_9408,plain,
! [X0: $i,X1: $i] : f(f(X0,X0),f(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_9312,c_6258]) ).
tcf(c_9638,plain,
! [X0: $i] : f(iPr_def_13,f(iPr_def_14,X0)) = iPr_def_14,
inference(superposition,[status(thm)],[c_3031,c_9408]) ).
tcf(c_9720,plain,
! [X0: $i,X1: $i] : f(f(f(X0,X1),f(X0,X1)),X0) = f(X0,X1),
inference(superposition,[status(thm)],[c_6258,c_9408]) ).
tcf(c_9765,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X0,X0),X1)) = f(X0,X0),
inference(superposition,[status(thm)],[c_9408,c_9408]) ).
tcf(c_10027,plain,
f(iPr_def_15,iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_6258,c_8001]) ).
tcf(c_10096,plain,
f(iPr_def_14,f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_10027,c_6258]) ).
tcf(c_10174,plain,
f(iPr_def_13,iPr_def_15) = iPr_def_14,
inference(superposition,[status(thm)],[c_10096,c_9638]) ).
tcf(c_10176,plain,
f(iPr_def_14,f(iPr_def_15,f(f(iPr_def_15,iPr_def_15),iPr_def_15))) = iPr_def_15,
inference(superposition,[status(thm)],[c_10096,c_1796]) ).
tcf(c_10306,plain,
f(iPr_def_12,iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_6258,c_8003]) ).
tcf(c_10375,plain,
f(iPr_def_11,f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_10306,c_6258]) ).
tcf(c_10455,plain,
f(iPr_def_11,f(iPr_def_12,f(f(iPr_def_12,iPr_def_12),iPr_def_12))) = iPr_def_12,
inference(superposition,[status(thm)],[c_10375,c_1794]) ).
tcf(c_11565,plain,
! [X0: $i] : f(iPr_def_14,f(iPr_def_15,f(f(iPr_def_15,f(f(iPr_def_13,iPr_def_13),iPr_def_13)),X0))) = iPr_def_15,
inference(superposition,[status(thm)],[c_10174,c_6145]) ).
tcf(c_11667,plain,
! [X0: $i,X1: $i] : f(f(X0,f(X1,X1)),f(f(X1,X1),f(X1,X1))) = f(X1,X1),
inference(superposition,[status(thm)],[c_7912,c_6145]) ).
tcf(c_11686,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X1,X0),f(X1,X0))) = f(X1,X0),
inference(superposition,[status(thm)],[c_6145,c_6258]) ).
tcf(c_11695,plain,
! [X0: $i,X1: $i] : f(f(X0,X1),f(X1,f(f(X0,X0),X0))) = X1,
inference(superposition,[status(thm)],[c_6145,c_6145]) ).
tcf(c_11761,plain,
! [X0: $i] : f(iPr_def_14,f(iPr_def_15,f(f(iPr_def_15,f(iPr_def_14,iPr_def_13)),X0))) = iPr_def_15,
inference(demodulation,[status(thm)],[c_11565,c_7604]) ).
tcf(c_11763,plain,
! [X0: $i,X1: $i] : f(f(X0,f(X1,X1)),X1) = f(X1,X1),
inference(demodulation,[status(thm)],[c_11667,c_9408]) ).
tcf(c_14147,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,X1)) = X1,
inference(superposition,[status(thm)],[c_68,c_6159]) ).
tcf(c_14158,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_10,f(x2,X0)),X1),f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_107,c_6159]) ).
tcf(c_14159,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_13,f(x2,X0)),X1),f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_108,c_6159]) ).
tcf(c_14161,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_12,f(iPr_def_11,X0)),X1),f(iPr_def_11,iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_110,c_6159]) ).
tcf(c_14163,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_15,f(iPr_def_14,X0)),X1),f(iPr_def_14,iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_112,c_6159]) ).
tcf(c_14165,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,x1),iPr_def_10),X1),f(x1,x1)) = x1,
inference(superposition,[status(thm)],[c_114,c_6159]) ).
tcf(c_14166,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,x0),iPr_def_13),X1),f(x0,x0)) = x0,
inference(superposition,[status(thm)],[c_115,c_6159]) ).
tcf(c_14384,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_15,f(iPr_def_14,X0)),X1),iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_14163,c_3031]) ).
tcf(c_14385,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_12,f(iPr_def_11,X0)),X1),iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_14161,c_3032]) ).
tcf(c_14471,plain,
! [X0: $i] : f(f(f(iPr_def_15,iPr_def_15),X0),iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_10176,c_14384]) ).
tcf(c_14627,plain,
! [X0: $i] : f(f(f(iPr_def_12,iPr_def_12),X0),iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_10455,c_14385]) ).
tcf(c_15507,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(X0,X0),f(f(f(X1,X0),f(X0,X2)),X3)) = X0,
inference(superposition,[status(thm)],[c_68,c_9720]) ).
tcf(c_15598,plain,
! [X0: $i,X1: $i] : f(f(f(X0,X0),f(X0,X0)),f(X1,f(X0,X0))) = f(X0,X0),
inference(superposition,[status(thm)],[c_11763,c_9720]) ).
tcf(c_15638,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_14,iPr_def_14),f(f(iPr_def_15,f(iPr_def_14,X0)),X1)) = iPr_def_14,
inference(superposition,[status(thm)],[c_14384,c_9720]) ).
tcf(c_15639,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_11,iPr_def_11),f(f(iPr_def_12,f(iPr_def_11,X0)),X1)) = iPr_def_11,
inference(superposition,[status(thm)],[c_14385,c_9720]) ).
tcf(c_15709,plain,
! [X0: $i,X1: $i] : f(iPr_def_10,f(f(iPr_def_12,f(iPr_def_11,X0)),X1)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_15639,c_3032]) ).
tcf(c_15710,plain,
! [X0: $i,X1: $i] : f(iPr_def_13,f(f(iPr_def_15,f(iPr_def_14,X0)),X1)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_15638,c_3031]) ).
tcf(c_15712,plain,
! [X0: $i,X1: $i] : f(X0,f(X1,f(X0,X0))) = f(X0,X0),
inference(demodulation,[status(thm)],[c_15598,c_9408]) ).
tcf(c_17478,plain,
! [X0: $i,X1: $i] : f(f(f(x0,f(iPr_def_12,X0)),X1),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_9405,c_14147]) ).
tcf(c_17479,plain,
! [X0: $i,X1: $i] : f(f(f(x1,f(iPr_def_15,X0)),X1),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_9404,c_14147]) ).
tcf(c_18288,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_14,iPr_def_14),f(f(f(X0,iPr_def_14),iPr_def_15),X1)) = iPr_def_14,
inference(superposition,[status(thm)],[c_10176,c_15507]) ).
tcf(c_18378,plain,
! [X0: $i,X1: $i] : f(iPr_def_13,f(f(f(X0,iPr_def_14),iPr_def_15),X1)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_18288,c_3031]) ).
tcf(c_22806,plain,
! [X0: $i,X1: $i] : f(iPr_def_13,f(f(f(iPr_def_14,X0),iPr_def_15),X1)) = iPr_def_14,
inference(superposition,[status(thm)],[c_9720,c_18378]) ).
tcf(c_26119,plain,
! [X0: $i,X1: $i] : f(iPr_def_10,f(f(iPr_def_12,f(X0,iPr_def_11)),X1)) = iPr_def_11,
inference(superposition,[status(thm)],[c_11686,c_15709]) ).
tcf(c_26145,plain,
! [X0: $i,X1: $i] : f(iPr_def_13,f(f(iPr_def_15,f(X0,iPr_def_14)),X1)) = iPr_def_14,
inference(superposition,[status(thm)],[c_11686,c_15710]) ).
tcf(c_26152,plain,
! [X0: $i,X1: $i] : f(iPr_def_13,f(X0,f(iPr_def_15,f(iPr_def_14,X1)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_11686,c_15710]) ).
tcf(c_26207,plain,
! [X0: $i] : f(f(X0,f(iPr_def_12,iPr_def_12)),iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_11686,c_14627]) ).
tcf(c_26209,plain,
! [X0: $i] : f(f(X0,f(iPr_def_15,iPr_def_15)),iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_11686,c_14471]) ).
tcf(c_26603,plain,
! [X0: $i] : f(iPr_def_11,f(iPr_def_12,f(f(iPr_def_12,f(f(X0,X0),X0)),iPr_def_12))) = iPr_def_12,
inference(superposition,[status(thm)],[c_26207,c_68]) ).
tcf(c_26785,plain,
! [X0: $i] : f(iPr_def_14,f(iPr_def_15,f(f(iPr_def_15,f(f(X0,X0),X0)),iPr_def_15))) = iPr_def_15,
inference(superposition,[status(thm)],[c_26209,c_68]) ).
tcf(c_28442,plain,
! [X0: $i,X1: $i] : f(iPr_def_10,f(X0,f(iPr_def_12,f(X1,iPr_def_11)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_11686,c_26119]) ).
tcf(c_30489,plain,
! [X0: $i,X1: $i] : f(iPr_def_13,f(X0,f(iPr_def_15,f(X1,iPr_def_14)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_11686,c_26145]) ).
tcf(c_42646,plain,
! [X0: $i] : f(f(iPr_def_11,X0),f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_28442,c_14158]) ).
tcf(c_42792,plain,
f(iPr_def_12,f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_26603,c_42646]) ).
tcf(c_42885,plain,
f(f(iPr_def_12,iPr_def_12),x2) = iPr_def_12,
inference(superposition,[status(thm)],[c_42792,c_9408]) ).
tcf(c_42974,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_12,f(x2,X0)),X1),f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_42885,c_14147]) ).
tcf(c_44036,plain,
! [X0: $i] : f(f(iPr_def_14,X0),f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_26152,c_14159]) ).
tcf(c_44191,plain,
f(iPr_def_15,f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_26785,c_44036]) ).
tcf(c_44281,plain,
f(f(x2,x2),iPr_def_15) = x2,
inference(superposition,[status(thm)],[c_44191,c_9720]) ).
tcf(c_44285,plain,
f(x2,f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_44191,c_6258]) ).
tcf(c_44321,plain,
f(x2,f(iPr_def_15,f(f(f(x2,x2),f(x2,x2)),f(x2,x2)))) = iPr_def_15,
inference(superposition,[status(thm)],[c_44281,c_11695]) ).
tcf(c_44349,plain,
f(x2,f(iPr_def_15,f(x2,f(x2,x2)))) = iPr_def_15,
inference(demodulation,[status(thm)],[c_44321,c_9408]) ).
tcf(c_44446,plain,
! [X0: $i] : f(x2,f(iPr_def_15,f(f(iPr_def_15,f(iPr_def_11,iPr_def_10)),X0))) = iPr_def_15,
inference(superposition,[status(thm)],[c_44285,c_210]) ).
tcf(c_46263,plain,
! [X0: $i] : f(f(iPr_def_11,X0),f(x1,x1)) = x1,
inference(superposition,[status(thm)],[c_14385,c_14165]) ).
tcf(c_46398,plain,
f(iPr_def_12,f(x1,x1)) = x1,
inference(superposition,[status(thm)],[c_26603,c_46263]) ).
tcf(c_46493,plain,
f(f(x1,x1),iPr_def_12) = x1,
inference(superposition,[status(thm)],[c_46398,c_9720]) ).
tcf(c_46533,plain,
! [X0: $i,X1: $i] : f(f(f(x1,f(iPr_def_12,X0)),X1),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_46493,c_14147]) ).
tcf(c_47413,plain,
! [X0: $i] : f(f(iPr_def_14,X0),f(x0,x0)) = x0,
inference(superposition,[status(thm)],[c_14384,c_14166]) ).
tcf(c_47547,plain,
f(iPr_def_15,f(x0,x0)) = x0,
inference(superposition,[status(thm)],[c_26785,c_47413]) ).
tcf(c_47637,plain,
f(f(x0,x0),iPr_def_15) = x0,
inference(superposition,[status(thm)],[c_47547,c_9720]) ).
tcf(c_47677,plain,
! [X0: $i,X1: $i] : f(f(f(x0,f(iPr_def_15,X0)),X1),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_47637,c_14147]) ).
tcf(c_62225,plain,
! [X0: $i] : f(f(f(x0,x2),X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_42792,c_17478]) ).
tcf(c_62282,plain,
! [X0: $i] : f(f(iPr_def_13,X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_62225,c_64]) ).
tcf(c_62353,plain,
f(iPr_def_14,f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_30489,c_62282]) ).
tcf(c_62406,plain,
f(iPr_def_12,iPr_def_13) = f(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_62282,c_7912]) ).
tcf(c_62420,plain,
f(iPr_def_12,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_62406,c_7604]) ).
tcf(c_62804,plain,
f(f(iPr_def_12,iPr_def_12),iPr_def_14) = iPr_def_12,
inference(superposition,[status(thm)],[c_62420,c_9408]) ).
tcf(c_62970,plain,
! [X0: $i] : f(iPr_def_13,f(f(iPr_def_12,iPr_def_15),X0)) = iPr_def_14,
inference(superposition,[status(thm)],[c_62353,c_22806]) ).
tcf(c_63018,plain,
f(iPr_def_12,f(iPr_def_14,f(f(f(iPr_def_12,iPr_def_12),f(iPr_def_12,iPr_def_12)),f(iPr_def_12,iPr_def_12)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_62804,c_11695]) ).
tcf(c_63063,plain,
f(iPr_def_12,f(iPr_def_14,f(iPr_def_12,f(iPr_def_12,iPr_def_12)))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_63018,c_9408]) ).
tcf(c_63390,plain,
f(f(iPr_def_12,iPr_def_15),f(iPr_def_12,iPr_def_15)) = f(iPr_def_14,f(iPr_def_12,iPr_def_15)),
inference(superposition,[status(thm)],[c_62970,c_11763]) ).
tcf(c_71043,plain,
! [X0: $i] : f(f(f(x1,x2),X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_44191,c_17479]) ).
tcf(c_71101,plain,
! [X0: $i] : f(f(iPr_def_10,X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_71043,c_61]) ).
tcf(c_71212,plain,
f(iPr_def_11,f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_28442,c_71101]) ).
tcf(c_71522,plain,
! [X0: $i] : f(iPr_def_10,f(f(iPr_def_12,iPr_def_15),X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_71212,c_15709]) ).
tcf(c_72253,plain,
f(f(iPr_def_12,iPr_def_15),f(iPr_def_12,iPr_def_15)) = f(iPr_def_11,f(iPr_def_12,iPr_def_15)),
inference(superposition,[status(thm)],[c_71522,c_11763]) ).
tcf(c_72254,plain,
f(f(iPr_def_12,iPr_def_15),f(iPr_def_12,iPr_def_15)) = f(f(iPr_def_12,iPr_def_15),iPr_def_11),
inference(superposition,[status(thm)],[c_71522,c_15712]) ).
tcf(c_72258,plain,
f(f(iPr_def_12,iPr_def_15),iPr_def_11) = f(iPr_def_14,f(iPr_def_12,iPr_def_15)),
inference(light_normalisation,[status(thm)],[c_72254,c_63390]) ).
tcf(c_102223,plain,
! [X0: $i] : f(f(f(iPr_def_12,iPr_def_15),X0),f(x2,x2)) = x2,
inference(superposition,[status(thm)],[c_44349,c_42974]) ).
tcf(c_102618,plain,
f(f(iPr_def_12,iPr_def_15),f(iPr_def_12,iPr_def_15)) = f(x2,f(iPr_def_12,iPr_def_15)),
inference(superposition,[status(thm)],[c_102223,c_7912]) ).
tcf(c_102631,plain,
f(x2,f(iPr_def_12,iPr_def_15)) = f(iPr_def_11,f(iPr_def_12,iPr_def_15)),
inference(light_normalisation,[status(thm)],[c_102618,c_72253]) ).
tcf(c_114412,plain,
! [X0: $i] : f(f(f(x1,iPr_def_14),X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_63063,c_46533]) ).
tcf(c_114473,plain,
! [X0: $i] : f(f(iPr_def_15,X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_114412,c_66]) ).
tcf(c_114512,plain,
! [X0: $i] : f(f(X0,iPr_def_15),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_11686,c_114473]) ).
tcf(c_114575,plain,
f(iPr_def_15,iPr_def_12) = f(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_114473,c_9765]) ).
tcf(c_114576,plain,
f(iPr_def_12,iPr_def_15) = f(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_114473,c_7912]) ).
tcf(c_114587,plain,
f(iPr_def_14,f(iPr_def_15,iPr_def_12)) = iPr_def_15,
inference(superposition,[status(thm)],[c_114473,c_11761]) ).
tcf(c_114588,plain,
f(x2,f(iPr_def_15,iPr_def_12)) = iPr_def_15,
inference(superposition,[status(thm)],[c_114473,c_44446]) ).
tcf(c_114928,plain,
f(iPr_def_12,iPr_def_15) = f(iPr_def_15,iPr_def_12),
inference(demodulation,[status(thm)],[c_114575,c_114576]) ).
tcf(c_115066,plain,
f(iPr_def_14,f(iPr_def_12,iPr_def_15)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_114587,c_114928]) ).
tcf(c_115068,plain,
f(f(iPr_def_12,iPr_def_15),iPr_def_11) = iPr_def_15,
inference(demodulation,[status(thm)],[c_72258,c_115066]) ).
tcf(c_115153,plain,
f(iPr_def_11,f(iPr_def_12,iPr_def_15)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_114588,c_102631,c_114928]) ).
tcf(c_115521,plain,
f(iPr_def_15,f(iPr_def_11,f(f(f(iPr_def_12,iPr_def_15),f(iPr_def_12,iPr_def_15)),f(iPr_def_12,iPr_def_15)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_115068,c_11695]) ).
tcf(c_115583,plain,
f(iPr_def_15,f(iPr_def_11,f(iPr_def_15,f(iPr_def_12,iPr_def_15)))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_115521,c_72253,c_115153]) ).
tcf(c_115858,plain,
! [X0: $i] : f(f(iPr_def_12,iPr_def_12),f(X0,iPr_def_15)) = iPr_def_12,
inference(superposition,[status(thm)],[c_114512,c_9720]) ).
tcf(c_132155,plain,
! [X0: $i] : f(f(f(x0,iPr_def_11),X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_115583,c_47677]) ).
tcf(c_132207,plain,
! [X0: $i] : f(f(iPr_def_12,X0),f(iPr_def_12,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_132155,c_63,c_114576]) ).
tcf(c_132445,plain,
iPr_def_12 = iPr_def_15,
inference(superposition,[status(thm)],[c_132207,c_115858]) ).
tcf(c_132446,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_132445,c_67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT393-2 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n004.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 : Wed Sep 23 21:32:21 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running UEQ theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/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.42 % Proving...
% 249.14/37.30 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 249.14/37.30 % SZS status Started for theBenchmark.p
% 249.14/37.30 % SZS status Unsatisfiable for theBenchmark.p
% 249.14/37.30
% 249.14/37.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 249.14/37.30
% 249.14/37.30 % ------ iProver source info
% 249.14/37.30
% 249.14/37.30 % git: date: 2026-07-19 20:42:38 +0200
% 249.14/37.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 249.14/37.30 % git: non_committed_changes: false
% 249.14/37.30
% 249.14/37.30 % ------ Parsing...% successful
% 249.14/37.30
% 249.14/37.30
% 249.14/37.30 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 249.14/37.30
% 249.14/37.30 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 249.14/37.30
% 249.14/37.30 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 249.14/37.30
% 249.14/37.30 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 249.14/37.30 % ------ Proving...
% 249.14/37.30 % ------ Problem Properties
% 249.14/37.30
% 249.14/37.30 %
% 249.14/37.30 % clauses 8
% 249.14/37.30 % conjectures 1
% 249.14/37.30 % EPR 1
% 249.14/37.30 % Horn 8
% 249.14/37.30 % unary 8
% 249.14/37.30 % binary 0
% 249.14/37.30 % lits 8
% 249.14/37.30 % lits eq 8
% 249.14/37.30 % fd_pure 0
% 249.14/37.30 % fd_pseudo 0
% 249.14/37.30 % fd_cond 0
% 249.14/37.30 % fd_pseudo_cond 0
% 249.14/37.30 % AC symbols 0
% 249.14/37.30
% 249.14/37.30 % ------ Input Options Time Limit: Unbounded
% 249.14/37.30
% 249.14/37.30
% 249.14/37.30 % ------
% 249.14/37.30 % Current options:
% 249.14/37.30 % ------
% 249.14/37.30
% 249.14/37.30
% 249.14/37.30 %
% 249.14/37.30
% 249.14/37.30 % ------ Proving...
% 249.14/37.30 %
% 249.14/37.30
% 249.14/37.30 % SZS status Unsatisfiable for theBenchmark.p
% 249.14/37.30
% 249.14/37.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 249.14/37.30
% 249.14/37.30
%------------------------------------------------------------------------------