%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT072-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.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:58:12 PM UTC 2026
% Result : Unsatisfiable 92.82s 20.77s
% Output : CNFRefutation 92.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 8
% Syntax : Number of formulae : 161 ( 161 unt; 6 def)
% Number of atoms : 615 ( 160 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 10 ( 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 : 230 ( 0 sgn 230 !; 0 ?; 226 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',oml_23A) ).
fof(f2,negated_conjecture,
f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity) ).
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(X2,f(f(X1,X1),X2)),X2))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
f(a,f(f(b,c),f(b,c))) != f(c,f(f(b,a),f(b,a))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,definition,
iPr_def_10 = f(b,c),
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(a,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_64,definition,
iPr_def_13 = f(b,a),
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(c,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(X2,f(f(X1,X1),X2)),X2))) = X1,
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_10,f(c,X0)),X1),f(c,f(f(X0,f(f(c,c),X0)),X0))) = c,
inference(superposition,[status(thm)],[c_61,c_68]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_13,f(a,X0)),X1),f(a,f(f(X0,f(f(a,a),X0)),X0))) = a,
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(X0,f(iPr_def_11,X0)),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(X0,f(f(iPr_def_11,iPr_def_11),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(X0,f(iPr_def_14,X0)),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(X0,f(f(iPr_def_14,iPr_def_14),X0)),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,b),iPr_def_10),X1),f(b,f(f(c,f(f(b,b),c)),c))) = b,
inference(superposition,[status(thm)],[c_61,c_68]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,b),iPr_def_13),X1),f(b,f(f(a,f(f(b,b),a)),a))) = b,
inference(superposition,[status(thm)],[c_64,c_68]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,iPr_def_10),f(iPr_def_10,X1)),X2),f(iPr_def_10,f(f(X1,f(iPr_def_11,X1)),X1))) = iPr_def_10,
inference(superposition,[status(thm)],[c_62,c_68]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,iPr_def_13),f(iPr_def_13,X1)),X2),f(iPr_def_13,f(f(X1,f(iPr_def_14,X1)),X1))) = iPr_def_13,
inference(superposition,[status(thm)],[c_65,c_68]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i] : f(X0,f(f(X0,X1),f(f(X2,f(f(f(X0,X1),f(X0,X1)),X2)),X2))) = 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_163,plain,
! [X0: $i] : f(iPr_def_10,f(iPr_def_11,f(f(X0,f(f(iPr_def_11,iPr_def_11),X0)),X0))) = iPr_def_11,
inference(superposition,[status(thm)],[c_147,c_68]) ).
tcf(c_178,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_194,plain,
! [X0: $i] : f(iPr_def_13,f(iPr_def_14,f(f(X0,f(f(iPr_def_14,iPr_def_14),X0)),X0))) = iPr_def_14,
inference(superposition,[status(thm)],[c_178,c_68]) ).
tcf(c_225,plain,
! [X0: $i] : f(f(f(iPr_def_10,iPr_def_15),X0),f(c,f(f(iPr_def_14,f(f(c,c),iPr_def_14)),iPr_def_14))) = c,
inference(superposition,[status(thm)],[c_66,c_107]) ).
tcf(c_240,plain,
! [X0: $i] : f(c,f(iPr_def_15,f(f(X0,f(f(iPr_def_15,iPr_def_15),X0)),X0))) = iPr_def_15,
inference(superposition,[status(thm)],[c_225,c_68]) ).
tcf(c_277,plain,
! [X0: $i] : f(f(f(iPr_def_13,iPr_def_12),X0),f(a,f(f(iPr_def_11,f(f(a,a),iPr_def_11)),iPr_def_11))) = a,
inference(superposition,[status(thm)],[c_63,c_108]) ).
tcf(c_292,plain,
! [X0: $i] : f(a,f(iPr_def_12,f(f(X0,f(f(iPr_def_12,iPr_def_12),X0)),X0))) = iPr_def_12,
inference(superposition,[status(thm)],[c_277,c_68]) ).
tcf(c_489,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X4,f(f(X1,X1),X4)),X4))) = X1,
inference(superposition,[status(thm)],[c_68,c_126]) ).
tcf(c_497,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(iPr_def_10,f(c,X0)),X1),f(c,f(f(X2,f(f(c,c),X2)),X2))) = c,
inference(superposition,[status(thm)],[c_107,c_126]) ).
tcf(c_498,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(iPr_def_13,f(a,X0)),X1),f(a,f(f(X2,f(f(a,a),X2)),X2))) = a,
inference(superposition,[status(thm)],[c_108,c_126]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(iPr_def_12,f(iPr_def_11,X0)),X1),f(iPr_def_11,f(f(X2,f(f(iPr_def_11,iPr_def_11),X2)),X2))) = iPr_def_11,
inference(superposition,[status(thm)],[c_110,c_126]) ).
tcf(c_502,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(iPr_def_15,f(iPr_def_14,X0)),X1),f(iPr_def_14,f(f(X2,f(f(iPr_def_14,iPr_def_14),X2)),X2))) = iPr_def_14,
inference(superposition,[status(thm)],[c_112,c_126]) ).
tcf(c_503,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,b),iPr_def_10),X1),f(b,f(f(X2,f(f(b,b),X2)),X2))) = b,
inference(superposition,[status(thm)],[c_114,c_126]) ).
tcf(c_504,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,b),iPr_def_13),X1),f(b,f(f(X2,f(f(b,b),X2)),X2))) = b,
inference(superposition,[status(thm)],[c_115,c_126]) ).
tcf(c_509,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,iPr_def_10),f(iPr_def_10,X1)),X2),f(iPr_def_10,f(f(X3,f(f(iPr_def_10,iPr_def_10),X3)),X3))) = iPr_def_10,
inference(superposition,[status(thm)],[c_121,c_126]) ).
tcf(c_510,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,iPr_def_13),f(iPr_def_13,X1)),X2),f(iPr_def_13,f(f(X3,f(f(iPr_def_13,iPr_def_13),X3)),X3))) = iPr_def_13,
inference(superposition,[status(thm)],[c_122,c_126]) ).
tcf(c_515,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_10,iPr_def_15),X0),f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(superposition,[status(thm)],[c_225,c_126]) ).
tcf(c_517,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_13,iPr_def_12),X0),f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(superposition,[status(thm)],[c_277,c_126]) ).
tcf(c_573,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,iPr_def_13),f(iPr_def_13,X1)),X2),f(iPr_def_13,f(f(X3,f(iPr_def_14,X3)),X3))) = iPr_def_13,
inference(demodulation,[status(thm)],[c_510,c_65]) ).
tcf(c_574,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,iPr_def_10),f(iPr_def_10,X1)),X2),f(iPr_def_10,f(f(X3,f(iPr_def_11,X3)),X3))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_509,c_62]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_13,X0),f(iPr_def_13,f(f(X1,f(iPr_def_14,X1)),X1))) = iPr_def_13,
inference(superposition,[status(thm)],[c_573,c_573]) ).
tcf(c_754,plain,
! [X0: $i] : f(iPr_def_14,f(iPr_def_13,f(f(X0,f(iPr_def_14,X0)),X0))) = iPr_def_13,
inference(superposition,[status(thm)],[c_194,c_749]) ).
tcf(c_760,plain,
! [X0: $i] : f(iPr_def_13,f(a,f(f(X0,f(f(a,a),X0)),X0))) = a,
inference(superposition,[status(thm)],[c_749,c_517]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_15,iPr_def_13),X0),f(iPr_def_14,f(f(X1,f(f(iPr_def_14,iPr_def_14),X1)),X1))) = iPr_def_14,
inference(superposition,[status(thm)],[c_754,c_502]) ).
tcf(c_788,plain,
! [X0: $i,X1: $i] : f(f(a,X0),f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(superposition,[status(thm)],[c_760,c_498]) ).
tcf(c_789,plain,
! [X0: $i] : f(a,f(iPr_def_13,f(f(X0,f(iPr_def_14,X0)),X0))) = iPr_def_13,
inference(superposition,[status(thm)],[c_760,c_749]) ).
tcf(c_791,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,iPr_def_13),a),X1),f(iPr_def_13,f(f(X2,f(iPr_def_14,X2)),X2))) = iPr_def_13,
inference(superposition,[status(thm)],[c_760,c_573]) ).
tcf(c_800,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_13,iPr_def_13),X0),f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(superposition,[status(thm)],[c_789,c_498]) ).
tcf(c_801,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_14,X0),f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(demodulation,[status(thm)],[c_800,c_65]) ).
tcf(c_814,plain,
! [X0: $i] : f(iPr_def_12,f(a,f(f(X0,f(f(a,a),X0)),X0))) = a,
inference(superposition,[status(thm)],[c_292,c_788]) ).
tcf(c_898,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_10,X0),f(iPr_def_10,f(f(X1,f(iPr_def_11,X1)),X1))) = iPr_def_10,
inference(superposition,[status(thm)],[c_574,c_574]) ).
tcf(c_903,plain,
! [X0: $i] : f(iPr_def_11,f(iPr_def_10,f(f(X0,f(iPr_def_11,X0)),X0))) = iPr_def_10,
inference(superposition,[status(thm)],[c_163,c_898]) ).
tcf(c_909,plain,
! [X0: $i] : f(iPr_def_10,f(c,f(f(X0,f(f(c,c),X0)),X0))) = c,
inference(superposition,[status(thm)],[c_898,c_515]) ).
tcf(c_925,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_12,iPr_def_10),X0),f(iPr_def_11,f(f(X1,f(f(iPr_def_11,iPr_def_11),X1)),X1))) = iPr_def_11,
inference(superposition,[status(thm)],[c_903,c_500]) ).
tcf(c_943,plain,
! [X0: $i,X1: $i] : f(f(c,X0),f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(superposition,[status(thm)],[c_909,c_497]) ).
tcf(c_944,plain,
! [X0: $i] : f(c,f(iPr_def_10,f(f(X0,f(iPr_def_11,X0)),X0))) = iPr_def_10,
inference(superposition,[status(thm)],[c_909,c_898]) ).
tcf(c_946,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(f(f(X0,iPr_def_10),c),X1),f(iPr_def_10,f(f(X2,f(iPr_def_11,X2)),X2))) = iPr_def_10,
inference(superposition,[status(thm)],[c_909,c_574]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i] : f(f(f(iPr_def_10,iPr_def_10),X0),f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(superposition,[status(thm)],[c_944,c_497]) ).
tcf(c_956,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_11,X0),f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(demodulation,[status(thm)],[c_955,c_62]) ).
tcf(c_966,plain,
! [X0: $i] : f(iPr_def_15,f(c,f(f(X0,f(f(c,c),X0)),X0))) = c,
inference(superposition,[status(thm)],[c_240,c_943]) ).
tcf(c_1246,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(X0,X1),f(X0,f(f(X2,f(f(X0,X0),X2)),X2))) = X0,
inference(superposition,[status(thm)],[c_489,c_489]) ).
tcf(c_1586,plain,
! [X0: $i,X1: $i,X2: $i] : f(f(X0,X1),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))) = X1,
inference(superposition,[status(thm)],[c_1246,c_489]) ).
tcf(c_1637,plain,
! [X0: $i] : f(iPr_def_15,f(iPr_def_14,f(f(X0,f(f(iPr_def_14,iPr_def_14),X0)),X0))) = iPr_def_14,
inference(superposition,[status(thm)],[c_1246,c_770]) ).
tcf(c_1639,plain,
! [X0: $i,X1: $i] : f(f(X0,iPr_def_13),f(iPr_def_13,f(f(X1,f(iPr_def_14,X1)),X1))) = iPr_def_13,
inference(superposition,[status(thm)],[c_1246,c_791]) ).
tcf(c_1640,plain,
! [X0: $i] : f(iPr_def_12,f(iPr_def_11,f(f(X0,f(f(iPr_def_11,iPr_def_11),X0)),X0))) = iPr_def_11,
inference(superposition,[status(thm)],[c_1246,c_925]) ).
tcf(c_1642,plain,
! [X0: $i,X1: $i] : f(f(X0,iPr_def_10),f(iPr_def_10,f(f(X1,f(iPr_def_11,X1)),X1))) = iPr_def_10,
inference(superposition,[status(thm)],[c_1246,c_946]) ).
tcf(c_1726,plain,
! [X0: $i] : f(iPr_def_14,f(iPr_def_15,f(f(X0,f(f(iPr_def_15,iPr_def_15),X0)),X0))) = iPr_def_15,
inference(superposition,[status(thm)],[c_1637,c_1246]) ).
tcf(c_1740,plain,
! [X0: $i,X1: $i] : f(f(X0,iPr_def_13),f(iPr_def_13,f(f(f(iPr_def_13,f(f(X1,f(iPr_def_14,X1)),X1)),iPr_def_13),f(iPr_def_13,f(f(X1,f(iPr_def_14,X1)),X1))))) = iPr_def_13,
inference(superposition,[status(thm)],[c_754,c_1639]) ).
tcf(c_1751,plain,
! [X0: $i] : f(f(X0,iPr_def_13),iPr_def_14) = iPr_def_13,
inference(demodulation,[status(thm)],[c_1740,c_65,c_1639]) ).
tcf(c_1757,plain,
f(iPr_def_14,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_65,c_1751]) ).
tcf(c_1792,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_14,X0),f(iPr_def_14,f(f(X1,f(iPr_def_13,X1)),X1))) = iPr_def_14,
inference(superposition,[status(thm)],[c_1757,c_1246]) ).
tcf(c_4557,plain,
! [X0: $i] : f(iPr_def_11,f(iPr_def_12,f(f(X0,f(f(iPr_def_12,iPr_def_12),X0)),X0))) = iPr_def_12,
inference(superposition,[status(thm)],[c_1640,c_1246]) ).
tcf(c_4577,plain,
! [X0: $i,X1: $i] : f(f(X0,iPr_def_10),f(iPr_def_10,f(f(f(iPr_def_10,f(f(X1,f(iPr_def_11,X1)),X1)),iPr_def_10),f(iPr_def_10,f(f(X1,f(iPr_def_11,X1)),X1))))) = iPr_def_10,
inference(superposition,[status(thm)],[c_903,c_1642]) ).
tcf(c_4593,plain,
! [X0: $i] : f(f(X0,iPr_def_10),iPr_def_11) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4577,c_62,c_1642]) ).
tcf(c_4600,plain,
f(iPr_def_11,iPr_def_11) = iPr_def_10,
inference(superposition,[status(thm)],[c_62,c_4593]) ).
tcf(c_4644,plain,
! [X0: $i,X1: $i] : f(f(iPr_def_11,X0),f(iPr_def_11,f(f(X1,f(iPr_def_10,X1)),X1))) = iPr_def_11,
inference(superposition,[status(thm)],[c_4600,c_1246]) ).
tcf(c_5267,plain,
! [X0: $i] : f(iPr_def_15,f(a,f(f(X0,f(f(a,a),X0)),X0))) = a,
inference(superposition,[status(thm)],[c_1726,c_801]) ).
tcf(c_5300,plain,
! [X0: $i] : f(f(iPr_def_14,X0),f(iPr_def_14,f(iPr_def_13,f(f(iPr_def_13,f(iPr_def_14,iPr_def_13)),iPr_def_13)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_1639,c_1792]) ).
tcf(c_5331,plain,
! [X0: $i] : f(f(iPr_def_14,X0),iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_5300,c_754]) ).
tcf(c_5418,plain,
f(iPr_def_13,iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_1757,c_5331]) ).
tcf(c_5837,plain,
! [X0: $i] : f(iPr_def_12,f(c,f(f(X0,f(f(c,c),X0)),X0))) = c,
inference(superposition,[status(thm)],[c_4557,c_956]) ).
tcf(c_5875,plain,
! [X0: $i] : f(f(iPr_def_11,X0),f(iPr_def_11,f(iPr_def_10,f(f(iPr_def_10,f(iPr_def_11,iPr_def_10)),iPr_def_10)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_1642,c_4644]) ).
tcf(c_5906,plain,
! [X0: $i] : f(f(iPr_def_11,X0),iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_5875,c_903]) ).
tcf(c_5997,plain,
f(iPr_def_10,iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_4600,c_5906]) ).
tcf(c_6753,plain,
! [X0: $i,X1: $i] : f(f(X0,X1),f(X1,f(f(X1,X1),f(f(f(X1,X1),f(f(f(X1,X1),f(X1,X1)),f(X1,X1))),f(X1,X1))))) = X1,
inference(superposition,[status(thm)],[c_1586,c_1586]) ).
tcf(c_6755,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X0,X1),f(f(f(X0,X1),f(X0,X1)),f(f(f(f(X0,X1),f(X0,X1)),f(f(f(f(X0,X1),f(X0,X1)),f(f(X0,X1),f(X0,X1))),f(f(X0,X1),f(X0,X1)))),f(f(X0,X1),f(X0,X1)))))) = f(X0,X1),
inference(superposition,[status(thm)],[c_1586,c_126]) ).
tcf(c_6757,plain,
! [X0: $i,X1: $i] : f(f(X0,X1),f(X0,f(f(X0,X0),f(f(f(X0,X0),f(f(f(X0,X0),f(X0,X0)),f(X0,X0))),f(X0,X0))))) = X0,
inference(superposition,[status(thm)],[c_1586,c_1246]) ).
tcf(c_6768,plain,
f(iPr_def_12,f(c,f(f(c,c),f(f(f(c,c),f(f(f(c,c),f(c,c)),f(c,c))),f(c,c))))) = c,
inference(superposition,[status(thm)],[c_1586,c_5837]) ).
tcf(c_6769,plain,
f(iPr_def_15,f(c,f(f(c,c),f(f(f(c,c),f(f(f(c,c),f(c,c)),f(c,c))),f(c,c))))) = c,
inference(superposition,[status(thm)],[c_1586,c_966]) ).
tcf(c_6775,plain,
f(iPr_def_15,f(a,f(f(a,a),f(f(f(a,a),f(f(f(a,a),f(a,a)),f(a,a))),f(a,a))))) = a,
inference(superposition,[status(thm)],[c_1586,c_5267]) ).
tcf(c_6776,plain,
f(iPr_def_12,f(a,f(f(a,a),f(f(f(a,a),f(f(f(a,a),f(a,a)),f(a,a))),f(a,a))))) = a,
inference(superposition,[status(thm)],[c_1586,c_814]) ).
tcf(c_6807,plain,
f(iPr_def_14,f(iPr_def_15,f(f(iPr_def_15,iPr_def_15),f(f(f(iPr_def_15,iPr_def_15),f(f(f(iPr_def_15,iPr_def_15),f(iPr_def_15,iPr_def_15)),f(iPr_def_15,iPr_def_15))),f(iPr_def_15,iPr_def_15))))) = iPr_def_15,
inference(superposition,[status(thm)],[c_1586,c_1726]) ).
tcf(c_6818,plain,
f(iPr_def_11,f(iPr_def_12,f(f(iPr_def_12,iPr_def_12),f(f(f(iPr_def_12,iPr_def_12),f(f(f(iPr_def_12,iPr_def_12),f(iPr_def_12,iPr_def_12)),f(iPr_def_12,iPr_def_12))),f(iPr_def_12,iPr_def_12))))) = iPr_def_12,
inference(superposition,[status(thm)],[c_1586,c_4557]) ).
tcf(c_6823,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,X1),f(f(f(X1,X1),f(f(f(X1,X1),f(X1,X1)),f(X1,X1))),f(X1,X1))))) = X1,
inference(superposition,[status(thm)],[c_1586,c_489]) ).
tcf(c_6834,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,b),iPr_def_13),X1),f(b,f(f(b,b),f(f(f(b,b),f(f(f(b,b),f(b,b)),f(b,b))),f(b,b))))) = b,
inference(superposition,[status(thm)],[c_1586,c_504]) ).
tcf(c_6835,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,b),iPr_def_10),X1),f(b,f(f(b,b),f(f(f(b,b),f(f(f(b,b),f(b,b)),f(b,b))),f(b,b))))) = b,
inference(superposition,[status(thm)],[c_1586,c_503]) ).
tcf(c_6865,plain,
f(iPr_def_11,f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_6818,c_126]) ).
tcf(c_6868,plain,
f(iPr_def_14,f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_6807,c_126]) ).
tcf(c_6871,plain,
f(iPr_def_12,f(a,a)) = a,
inference(demodulation,[status(thm)],[c_6776,c_126]) ).
tcf(c_6872,plain,
f(iPr_def_15,f(a,a)) = a,
inference(demodulation,[status(thm)],[c_6775,c_126]) ).
tcf(c_6874,plain,
f(iPr_def_15,f(c,c)) = c,
inference(demodulation,[status(thm)],[c_6769,c_126]) ).
tcf(c_6875,plain,
f(iPr_def_12,f(c,c)) = c,
inference(demodulation,[status(thm)],[c_6768,c_126]) ).
tcf(c_6878,plain,
! [X0: $i,X1: $i] : f(f(X0,X1),f(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_6757,c_126]) ).
tcf(c_6879,plain,
! [X0: $i,X1: $i] : f(f(X0,X1),f(X1,X1)) = X1,
inference(demodulation,[status(thm)],[c_6753,c_126]) ).
tcf(c_6887,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,b),iPr_def_10),X1),f(b,b)) = b,
inference(demodulation,[status(thm)],[c_6835,c_126]) ).
tcf(c_6888,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,b),iPr_def_13),X1),f(b,b)) = b,
inference(demodulation,[status(thm)],[c_6834,c_126]) ).
tcf(c_6893,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,X1)) = X1,
inference(demodulation,[status(thm)],[c_6823,c_126]) ).
tcf(c_6907,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X0,X1),f(X0,X1))) = f(X0,X1),
inference(demodulation,[status(thm)],[c_6755,c_126]) ).
tcf(c_7938,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X1,X0),f(X1,X0))) = f(X1,X0),
inference(superposition,[status(thm)],[c_1586,c_6878]) ).
tcf(c_8031,plain,
! [X0: $i,X1: $i] : f(f(f(X0,X0),X1),X0) = f(X0,X0),
inference(superposition,[status(thm)],[c_6878,c_6878]) ).
tcf(c_8210,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X0,f(f(X1,f(f(X0,X0),X1)),X1)),f(X0,f(f(X1,f(f(X0,X0),X1)),X1)))) = f(X0,f(f(X1,f(f(X0,X0),X1)),X1)),
inference(superposition,[status(thm)],[c_1586,c_6879]) ).
tcf(c_8383,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X1,f(f(X0,X0),X1)),X1)) = f(X0,X0),
inference(demodulation,[status(thm)],[c_8210,c_1246]) ).
tcf(c_8808,plain,
! [X0: $i] : f(f(iPr_def_11,X0),f(b,b)) = b,
inference(superposition,[status(thm)],[c_5906,c_6887]) ).
tcf(c_8831,plain,
f(iPr_def_12,f(b,b)) = b,
inference(superposition,[status(thm)],[c_6865,c_8808]) ).
tcf(c_8864,plain,
! [X0: $i] : f(f(iPr_def_14,X0),f(b,b)) = b,
inference(superposition,[status(thm)],[c_5331,c_6888]) ).
tcf(c_8887,plain,
f(iPr_def_15,f(b,b)) = b,
inference(superposition,[status(thm)],[c_6868,c_8864]) ).
tcf(c_17770,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,iPr_def_12),a),X1),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_6871,c_6893]) ).
tcf(c_17771,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,iPr_def_15),a),X1),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_6872,c_6893]) ).
tcf(c_17773,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,iPr_def_15),c),X1),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_6874,c_6893]) ).
tcf(c_17774,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,iPr_def_12),c),X1),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_6875,c_6893]) ).
tcf(c_17807,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,iPr_def_12),b),X1),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_8831,c_6893]) ).
tcf(c_17813,plain,
! [X0: $i,X1: $i] : f(f(f(f(X0,iPr_def_15),b),X1),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_8887,c_6893]) ).
tcf(c_21154,plain,
! [X0: $i] : f(f(f(a,a),X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_8031,c_17771]) ).
tcf(c_24015,plain,
! [X0: $i] : f(f(f(c,c),X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_8031,c_17774]) ).
tcf(c_24202,plain,
! [X0: $i] : f(f(f(b,b),X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_8031,c_17807]) ).
tcf(c_24557,plain,
! [X0: $i] : f(f(f(b,b),X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_8031,c_17813]) ).
tcf(c_31310,plain,
! [X0: $i,X1: $i] : f(X0,f(f(f(f(f(X0,X0),X1),f(f(X0,X0),X1)),f(f(X0,X0),X1)),f(f(f(X0,X0),X1),f(f(X0,X0),X1)))) = f(X0,X0),
inference(superposition,[status(thm)],[c_6907,c_8383]) ).
tcf(c_31312,plain,
! [X0: $i,X1: $i] : f(X0,f(f(f(f(X1,f(X0,X0)),f(X1,f(X0,X0))),f(X1,f(X0,X0))),f(f(X1,f(X0,X0)),f(X1,f(X0,X0))))) = f(X0,X0),
inference(superposition,[status(thm)],[c_7938,c_8383]) ).
tcf(c_31455,plain,
f(f(a,a),f(f(f(iPr_def_15,iPr_def_15),iPr_def_15),f(iPr_def_15,iPr_def_15))) = f(f(a,a),f(a,a)),
inference(superposition,[status(thm)],[c_21154,c_8383]) ).
tcf(c_31462,plain,
f(f(c,c),f(f(f(iPr_def_12,iPr_def_12),iPr_def_12),f(iPr_def_12,iPr_def_12))) = f(f(c,c),f(c,c)),
inference(superposition,[status(thm)],[c_24015,c_8383]) ).
tcf(c_31465,plain,
f(f(b,b),f(f(f(iPr_def_12,iPr_def_12),iPr_def_12),f(iPr_def_12,iPr_def_12))) = f(f(b,b),f(b,b)),
inference(superposition,[status(thm)],[c_24202,c_8383]) ).
tcf(c_31471,plain,
f(f(b,b),f(f(f(iPr_def_15,iPr_def_15),iPr_def_15),f(iPr_def_15,iPr_def_15))) = f(f(b,b),f(b,b)),
inference(superposition,[status(thm)],[c_24557,c_8383]) ).
tcf(c_31768,plain,
f(f(b,b),iPr_def_15) = b,
inference(demodulation,[status(thm)],[c_31471,c_6878,c_6879]) ).
tcf(c_31770,plain,
f(f(b,b),iPr_def_12) = b,
inference(demodulation,[status(thm)],[c_31465,c_6878,c_6879]) ).
tcf(c_31771,plain,
f(f(c,c),iPr_def_12) = c,
inference(demodulation,[status(thm)],[c_31462,c_6878,c_6879]) ).
tcf(c_31773,plain,
f(f(a,a),iPr_def_15) = a,
inference(demodulation,[status(thm)],[c_31455,c_6878,c_6879]) ).
tcf(c_31919,plain,
! [X0: $i,X1: $i] : f(X0,f(X1,f(X0,X0))) = f(X0,X0),
inference(demodulation,[status(thm)],[c_31312,c_6879]) ).
tcf(c_31920,plain,
! [X0: $i,X1: $i] : f(X0,f(f(X0,X0),X1)) = f(X0,X0),
inference(demodulation,[status(thm)],[c_31310,c_6879]) ).
tcf(c_32299,plain,
! [X0: $i] : f(f(f(b,c),X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_31768,c_17773]) ).
tcf(c_32305,plain,
! [X0: $i] : f(f(iPr_def_10,X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_32299,c_61]) ).
tcf(c_32358,plain,
! [X0: $i] : f(f(f(b,a),X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_31770,c_17770]) ).
tcf(c_32363,plain,
! [X0: $i] : f(f(iPr_def_13,X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_32358,c_64]) ).
tcf(c_32368,plain,
! [X0: $i,X1: $i] : f(f(f(c,f(iPr_def_12,X0)),X1),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_31771,c_6893]) ).
tcf(c_32422,plain,
! [X0: $i,X1: $i] : f(f(f(a,f(iPr_def_15,X0)),X1),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_31773,c_6893]) ).
tcf(c_32777,plain,
f(iPr_def_10,iPr_def_10) = f(iPr_def_15,iPr_def_10),
inference(superposition,[status(thm)],[c_32305,c_8031]) ).
tcf(c_32794,plain,
f(iPr_def_15,iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_32777,c_5997]) ).
tcf(c_32988,plain,
f(iPr_def_12,iPr_def_13) = f(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_32363,c_8031]) ).
tcf(c_33004,plain,
f(iPr_def_12,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_32988,c_5418]) ).
tcf(c_35887,plain,
! [X0: $i,X1: $i] : f(f(X0,X0),f(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_6878,c_31919]) ).
tcf(c_37159,plain,
! [X0: $i,X1: $i] : f(f(X0,X0),f(X0,X1)) = X0,
inference(superposition,[status(thm)],[c_35887,c_31920]) ).
tcf(c_54421,plain,
! [X0: $i] : f(f(f(c,iPr_def_14),X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_33004,c_32368]) ).
tcf(c_54443,plain,
! [X0: $i] : f(f(iPr_def_15,X0),f(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_54421,c_66]) ).
tcf(c_54489,plain,
f(iPr_def_12,iPr_def_15) = f(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_54443,c_8031]) ).
tcf(c_68845,plain,
! [X0: $i] : f(f(f(a,iPr_def_11),X0),f(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(superposition,[status(thm)],[c_32794,c_32422]) ).
tcf(c_68872,plain,
! [X0: $i] : f(f(iPr_def_12,X0),f(iPr_def_12,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_68845,c_63,c_54489]) ).
tcf(c_68959,plain,
iPr_def_12 = iPr_def_15,
inference(superposition,[status(thm)],[c_68872,c_37159]) ).
tcf(c_68978,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_68959,c_67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT072-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 20:13:08 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running UEQ theorem proving
% 0.10/0.41 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.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 92.82/20.77 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 92.82/20.77 % SZS status Started for theBenchmark.p
% 92.82/20.77 % SZS status Unsatisfiable for theBenchmark.p
% 92.82/20.77
% 92.82/20.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 92.82/20.77
% 92.82/20.77 % ------ iProver source info
% 92.82/20.77
% 92.82/20.77 % git: date: 2026-07-19 20:42:38 +0200
% 92.82/20.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 92.82/20.77 % git: non_committed_changes: false
% 92.82/20.77
% 92.82/20.77 % ------ Parsing...% successful
% 92.82/20.77
% 92.82/20.77
% 92.82/20.77 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 92.82/20.77
% 92.82/20.77 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 92.82/20.77
% 92.82/20.77 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 92.82/20.77
% 92.82/20.77 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 92.82/20.77 % ------ Proving...
% 92.82/20.77 % ------ Problem Properties
% 92.82/20.77
% 92.82/20.77 %
% 92.82/20.77 % clauses 8
% 92.82/20.77 % conjectures 1
% 92.82/20.77 % EPR 1
% 92.82/20.77 % Horn 8
% 92.82/20.77 % unary 8
% 92.82/20.77 % binary 0
% 92.82/20.77 % lits 8
% 92.82/20.77 % lits eq 8
% 92.82/20.77 % fd_pure 0
% 92.82/20.77 % fd_pseudo 0
% 92.82/20.77 % fd_cond 0
% 92.82/20.77 % fd_pseudo_cond 0
% 92.82/20.77 % AC symbols 0
% 92.82/20.77
% 92.82/20.77 % ------ Input Options Time Limit: Unbounded
% 92.82/20.77
% 92.82/20.77
% 92.82/20.77 % ------
% 92.82/20.77 % Current options:
% 92.82/20.77 % ------
% 92.82/20.77
% 92.82/20.77
% 92.82/20.77 %
% 92.82/20.77
% 92.82/20.77 % ------ Proving...
% 92.82/20.77 %
% 92.82/20.77
% 92.82/20.77 % SZS status Unsatisfiable for theBenchmark.p
% 92.82/20.77
% 92.82/20.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 92.82/20.77
% 92.82/20.77
%------------------------------------------------------------------------------