%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL167-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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 02:05:49 PM UTC 2026
% Result : Unsatisfiable 93.32s 15.47s
% Output : CNFRefutation 93.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 3
% Syntax : Number of formulae : 203 ( 34 unt; 0 def)
% Number of atoms : 477 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 550 ( 276 ~; 274 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 561 ( 0 sgn 561 !; 0 ?; 556 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xhk) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(c,equivalent(equivalent(c,b),a)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_yro) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_54,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(c,equivalent(equivalent(c,b),a)))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_82,c_52]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_83,c_52]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X3,X2),X1)))) ),
inference(superposition,[status(thm)],[c_53,c_84]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),X3))) ),
inference(superposition,[status(thm)],[c_115,c_84]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X1)) ),
inference(superposition,[status(thm)],[c_115,c_131]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_173,c_52]) ).
tcf(c_178,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_174,c_145]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_178]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X3,equivalent(X2,X1)))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_173,c_178]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X3)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_174,c_178]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_173,c_197]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X0,X2),X1),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_132]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_248,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_238,c_201]) ).
tcf(c_249,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_238,c_52]) ).
tcf(c_252,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_206,c_201]) ).
tcf(c_286,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X3)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,X4),X2),X1)),X4))) ),
inference(superposition,[status(thm)],[c_53,c_198]) ).
tcf(c_288,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X3)
| ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_249,c_198]) ).
tcf(c_292,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),X3))) ),
inference(superposition,[status(thm)],[c_53,c_199]) ).
tcf(c_317,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_249,c_145]) ).
tcf(c_325,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X0,X3),X2),X1)),X3))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_248]) ).
tcf(c_555,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_556,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_559,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_556,c_201]) ).
tcf(c_622,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_252,c_201]) ).
tcf(c_654,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_622]) ).
tcf(c_668,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_654,c_555]) ).
tcf(c_692,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_325,c_145]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(equivalent(X0,X3),X3),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_692]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_556,c_692]) ).
tcf(c_799,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_771,c_559]) ).
tcf(c_807,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_799]) ).
tcf(c_826,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_807,c_559]) ).
tcf(c_832,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(superposition,[status(thm)],[c_53,c_826]) ).
tcf(c_873,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X1)) ),
inference(superposition,[status(thm)],[c_832,c_668]) ).
tcf(c_897,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X2,X3),X3),X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_770,c_52]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,X0)) ),
inference(superposition,[status(thm)],[c_897,c_873]) ).
tcf(c_2524,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_2525,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_2544,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(X3,equivalent(equivalent(equivalent(X2,X3),X1),X0)))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_2525,c_286]) ).
tcf(c_2586,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_252,c_201]) ).
tcf(c_2596,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_2586]) ).
tcf(c_2610,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_2596,c_2524]) ).
tcf(c_2671,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_2610]) ).
tcf(c_2754,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_206,c_2671]) ).
tcf(c_2964,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(equivalent(X2,X3),X3),X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_2754]) ).
tcf(c_2996,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_2544,c_2964]) ).
tcf(c_6017,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_6018,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_6021,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_6018,c_201]) ).
tcf(c_6022,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_6018,c_52]) ).
tcf(c_6052,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_252,c_201]) ).
tcf(c_6062,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_6052]) ).
tcf(c_6077,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_6062,c_6017]) ).
tcf(c_6095,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_325,c_145]) ).
tcf(c_6105,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X1)) ),
inference(superposition,[status(thm)],[c_53,c_292]) ).
tcf(c_6134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_6077]) ).
tcf(c_6182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(equivalent(X0,X3),X3),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_6095]) ).
tcf(c_6183,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_6018,c_6095]) ).
tcf(c_6201,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_6183,c_6021]) ).
tcf(c_6209,plain,
! [X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1) ),
inference(global_subsumption_just,[status(thm)],[c_6201,c_832,c_977]) ).
tcf(c_6210,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(renaming,[status(thm)],[c_6209]) ).
tcf(c_6220,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_6210,c_6021]) ).
tcf(c_6227,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(superposition,[status(thm)],[c_53,c_6220]) ).
tcf(c_6255,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X2,X3),X3),X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_6182,c_52]) ).
tcf(c_6286,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X3)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),equivalent(X3,X2)))) ),
inference(superposition,[status(thm)],[c_6255,c_6134]) ).
tcf(c_6328,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X0))) ),
inference(superposition,[status(thm)],[c_53,c_6286]) ).
tcf(c_6344,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),X2)) ),
inference(superposition,[status(thm)],[c_6022,c_6328]) ).
tcf(c_6546,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_325,c_6344]) ).
tcf(c_6553,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_6022,c_6546]) ).
tcf(c_6561,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,equivalent(X0,X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_6227,c_6546]) ).
tcf(c_6595,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X3,X2),X1)),X3))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_6553]) ).
tcf(c_6699,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0)),X2)),
inference(superposition,[status(thm)],[c_6227,c_6595]) ).
tcf(c_6926,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X2,X1),X0),X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_6699,c_6546]) ).
tcf(c_6931,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X1,X1),X0))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_6699,c_6105]) ).
tcf(c_6932,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X0,X0),X1)) ),
inference(superposition,[status(thm)],[c_6699,c_145]) ).
tcf(c_7043,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X1))) ),
inference(superposition,[status(thm)],[c_6931,c_6328]) ).
tcf(c_7057,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,equivalent(X1,X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_6561,c_6932]) ).
tcf(c_7082,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(equivalent(X0,X0)) ),
inference(superposition,[status(thm)],[c_6931,c_7043]) ).
tcf(c_8138,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_6926,c_6077]) ).
tcf(c_8487,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X1))) ),
inference(superposition,[status(thm)],[c_6931,c_8138]) ).
tcf(c_13370,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_13371,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_13374,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_13371,c_201]) ).
tcf(c_13410,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_252,c_201]) ).
tcf(c_13423,plain,
! [X0: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_13410,c_7057,c_8487]) ).
tcf(c_13424,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(renaming,[status(thm)],[c_13423]) ).
tcf(c_13432,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_13424,c_13370]) ).
tcf(c_13452,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_325,c_145]) ).
tcf(c_13489,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_13432]) ).
tcf(c_13494,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X3))) ),
inference(superposition,[status(thm)],[c_325,c_13432]) ).
tcf(c_13497,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13371,c_13452]) ).
tcf(c_13520,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13497,c_13374]) ).
tcf(c_13528,plain,
! [X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1) ),
inference(global_subsumption_just,[status(thm)],[c_13520,c_832,c_977]) ).
tcf(c_13529,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(renaming,[status(thm)],[c_13528]) ).
tcf(c_13539,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_13529,c_13374]) ).
tcf(c_13545,plain,
! [X1: $i] : is_a_theorem(equivalent(X1,X1)),
inference(global_subsumption_just,[status(thm)],[c_13539,c_832,c_7082]) ).
tcf(c_13546,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(renaming,[status(thm)],[c_13545]) ).
tcf(c_13585,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_206,c_13489]) ).
tcf(c_13707,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(equivalent(X2,X3),X3),X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_13585]) ).
tcf(c_14299,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X1,X2)) ),
inference(global_subsumption_just,[status(thm)],[c_288,c_2996]) ).
tcf(c_14300,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(renaming,[status(thm)],[c_14299]) ).
tcf(c_14849,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X0,X1)),X2))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_13494]) ).
tcf(c_14910,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X0))) ),
inference(superposition,[status(thm)],[c_14849,c_52]) ).
tcf(c_14920,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_14849,c_13432]) ).
tcf(c_14924,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_14849,c_13374]) ).
tcf(c_15129,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X2,X1),X0),X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_53,c_14920]) ).
tcf(c_15291,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_14924,c_14910]) ).
tcf(c_15497,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_15291]) ).
tcf(c_15542,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X0)),
inference(superposition,[status(thm)],[c_13546,c_15497]) ).
tcf(c_15620,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,X1),X2),X2)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_15542,c_14920]) ).
tcf(c_16053,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X1))) ),
inference(superposition,[status(thm)],[c_15620,c_13707]) ).
tcf(c_16161,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),X1)),
inference(superposition,[status(thm)],[c_15542,c_16053]) ).
tcf(c_16178,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X0,X0),X1)) ),
inference(superposition,[status(thm)],[c_16161,c_52]) ).
tcf(c_16340,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X2),X1),X0))),
inference(superposition,[status(thm)],[c_53,c_16178]) ).
tcf(c_16405,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_16340,c_14300]) ).
tcf(c_18747,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_15129,c_16405]) ).
tcf(c_18894,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0)),X2)),
inference(superposition,[status(thm)],[c_53,c_18747]) ).
tcf(c_19000,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X0,X1),X2))) ),
inference(superposition,[status(thm)],[c_18894,c_13432]) ).
tcf(c_25881,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X0),X1)),
inference(superposition,[status(thm)],[c_53,c_19000]) ).
tcf(c_25956,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X0),X1))),
inference(superposition,[status(thm)],[c_25881,c_18747]) ).
tcf(c_26492,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_25956,c_14910]) ).
tcf(c_27533,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_27534,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_27537,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_27534,c_201]) ).
tcf(c_27553,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_325,c_145]) ).
tcf(c_27564,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(equivalent(X0,X3),X3),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_27553]) ).
tcf(c_27565,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_27534,c_27553]) ).
tcf(c_27570,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_27565,c_27537]) ).
tcf(c_27576,plain,
! [X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),X2))
| ~ is_a_theorem(X1) ),
inference(global_subsumption_just,[status(thm)],[c_27570,c_832,c_977]) ).
tcf(c_27577,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(renaming,[status(thm)],[c_27576]) ).
tcf(c_27578,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_27577,c_201]) ).
tcf(c_27580,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_27577,c_27537]) ).
tcf(c_27584,plain,
! [X1: $i] : is_a_theorem(equivalent(X1,X1)),
inference(global_subsumption_just,[status(thm)],[c_27580,c_832,c_7082]) ).
tcf(c_27585,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(renaming,[status(thm)],[c_27584]) ).
tcf(c_27596,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_27578,c_27533]) ).
tcf(c_27670,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X3))) ),
inference(superposition,[status(thm)],[c_325,c_27596]) ).
tcf(c_27674,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X1)) ),
inference(superposition,[status(thm)],[c_27585,c_27596]) ).
tcf(c_28056,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X3)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_317]) ).
tcf(c_29275,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X0,X1)),X2))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_27670]) ).
tcf(c_29288,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_27564,c_27670]) ).
tcf(c_29311,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X0))) ),
inference(superposition,[status(thm)],[c_29275,c_52]) ).
tcf(c_29324,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_29275,c_27537]) ).
tcf(c_29334,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,equivalent(X0,X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_29275,c_27674]) ).
tcf(c_29462,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_29334,c_27670]) ).
tcf(c_30133,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_29324,c_29311]) ).
tcf(c_30139,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(global_subsumption_just,[status(thm)],[c_30133,c_26492]) ).
tcf(c_30142,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X0)),
inference(superposition,[status(thm)],[c_53,c_30139]) ).
tcf(c_30392,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_30142,c_29462]) ).
tcf(c_30417,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0)),X2)),
inference(superposition,[status(thm)],[c_53,c_30392]) ).
tcf(c_30461,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X0,X1),X1))),
inference(superposition,[status(thm)],[c_30142,c_30392]) ).
tcf(c_30491,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X1))) ),
inference(superposition,[status(thm)],[c_30461,c_28056]) ).
tcf(c_30646,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),X1)),
inference(superposition,[status(thm)],[c_30142,c_30491]) ).
tcf(c_30676,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X0,X0),X1)) ),
inference(superposition,[status(thm)],[c_30646,c_52]) ).
tcf(c_30711,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X2),X1),X0))),
inference(superposition,[status(thm)],[c_53,c_30676]) ).
tcf(c_30798,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X0),X1),X2),equivalent(X2,X1))),
inference(superposition,[status(thm)],[c_30711,c_30392]) ).
tcf(c_31127,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X2),X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X0)) ),
inference(superposition,[status(thm)],[c_30798,c_27596]) ).
tcf(c_32233,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X0),equivalent(equivalent(equivalent(X1,X2),X2),X1))),
inference(superposition,[status(thm)],[c_30417,c_31127]) ).
tcf(c_32510,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(equivalent(X0,X0)) ),
inference(superposition,[status(thm)],[c_32233,c_29288]) ).
tcf(c_58960,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0))) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_58961,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X0,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_58964,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_58961,c_201]) ).
tcf(c_58965,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X2,X1),X0))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_58961,c_52]) ).
tcf(c_58974,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X2,X3),equivalent(equivalent(equivalent(X0,X1),X3),X2)))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_325,c_201]) ).
tcf(c_58980,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_58974,c_58960]) ).
tcf(c_58992,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_58980,c_58960]) ).
tcf(c_59014,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_325,c_145]) ).
tcf(c_59024,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(equivalent(X2,X3),X1),X0)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_58992]) ).
tcf(c_59032,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(equivalent(X0,X3),X3),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_59014]) ).
tcf(c_59056,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X3,X2))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X0),X2),X3))) ),
inference(superposition,[status(thm)],[c_58965,c_59024]) ).
tcf(c_59066,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_59032,c_58960]) ).
tcf(c_59073,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X0)),X1)) ),
inference(superposition,[status(thm)],[c_53,c_59056]) ).
tcf(c_59148,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_59066,c_58964]) ).
tcf(c_59152,plain,
! [X1: $i] : is_a_theorem(equivalent(X1,X1)),
inference(global_subsumption_just,[status(thm)],[c_59148,c_832,c_7082]) ).
tcf(c_59153,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(renaming,[status(thm)],[c_59152]) ).
tcf(c_59169,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,X0))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_58965,c_59073]) ).
tcf(c_59278,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X0)) ),
inference(superposition,[status(thm)],[c_53,c_59169]) ).
tcf(c_59279,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,equivalent(X0,X1))) ),
inference(superposition,[status(thm)],[c_58961,c_59169]) ).
tcf(c_59307,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_58965,c_59278]) ).
tcf(c_59543,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),X2),X1)))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_53,c_59279]) ).
tcf(c_59555,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X0,X3),X2)),X1))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_53,c_59307]) ).
tcf(c_59578,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1))
| ~ is_a_theorem(X0) ),
inference(superposition,[status(thm)],[c_59543,c_52]) ).
tcf(c_59604,plain,
! [X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X2),X1)),
inference(global_subsumption_just,[status(thm)],[c_59578,c_832,c_32510]) ).
tcf(c_59605,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X0)),
inference(renaming,[status(thm)],[c_59604]) ).
tcf(c_59606,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X1),X2)) ),
inference(superposition,[status(thm)],[c_59605,c_59307]) ).
tcf(c_59680,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(X0,equivalent(equivalent(X0,X1),X1))),
inference(superposition,[status(thm)],[c_59153,c_59606]) ).
tcf(c_59695,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(equivalent(X1,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_59680,c_59169]) ).
tcf(c_59712,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X2,X1),X0)),X2)),
inference(superposition,[status(thm)],[c_53,c_59695]) ).
tcf(c_59777,plain,
! [X0: $i,X1: $i] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X0),X1)),
inference(superposition,[status(thm)],[c_59712,c_59278]) ).
tcf(c_60076,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X0)) ),
inference(superposition,[status(thm)],[c_59777,c_52]) ).
tcf(c_60245,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),X1))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_59555,c_60076]) ).
tcf(c_69155,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X0,X1),X2)),equivalent(X2,X1))),
inference(superposition,[status(thm)],[c_53,c_60245]) ).
tcf(c_69968,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,equivalent(equivalent(X2,X1),X0)))),
inference(superposition,[status(thm)],[c_69155,c_59695]) ).
tcf(c_70016,plain,
$false,
inference(superposition,[status(thm)],[c_69968,c_54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL167-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38 % Computer : n005.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Wed Sep 23 22:08:02 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.43
% 0.12/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.43
% 0.12/0.43 % Detected problem language: tptp
% 0.12/0.44 % Proving...
% 93.32/15.47 % SZS status Started for theBenchmark.p
% 93.32/15.47 % SZS status Unsatisfiable for theBenchmark.p
% 93.32/15.47
% 93.32/15.47 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 93.32/15.47
% 93.32/15.47 % ------ iProver source info
% 93.32/15.47
% 93.32/15.47 % git: date: 2026-07-19 20:42:38 +0200
% 93.32/15.47 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 93.32/15.47 % git: non_committed_changes: false
% 93.32/15.47
% 93.32/15.47 % ------ Parsing...% successful
% 93.32/15.47
% 93.32/15.47
% 93.32/15.47 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 93.32/15.47
% 93.32/15.47 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 93.32/15.47
% 93.32/15.47 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 93.32/15.47 % ------ Proving...
% 93.32/15.47 % ------ Problem Properties
% 93.32/15.47
% 93.32/15.47 %
% 93.32/15.47 % clauses 3
% 93.32/15.47 % conjectures 1
% 93.32/15.47 % EPR 0
% 93.32/15.47 % Horn 3
% 93.32/15.47 % unary 2
% 93.32/15.47 % binary 0
% 93.32/15.47 % lits 5
% 93.32/15.47 % lits eq 0
% 93.32/15.47 % fd_pure 0
% 93.32/15.47 % fd_pseudo 0
% 93.32/15.47 % fd_cond 0
% 93.32/15.47 % fd_pseudo_cond 0
% 93.32/15.47 % AC symbols 0
% 93.32/15.47
% 93.32/15.47 % ------ Input Options Time Limit: Unbounded
% 93.32/15.47
% 93.32/15.47
% 93.32/15.47 % ------
% 93.32/15.47 % Current options:
% 93.32/15.47 % ------
% 93.32/15.47
% 93.32/15.47
% 93.32/15.47 %
% 93.32/15.47
% 93.32/15.47 % ------ Proving...
% 93.32/15.47 %
% 93.32/15.47
% 93.32/15.47 % SZS status Unsatisfiable for theBenchmark.p
% 93.32/15.47
% 93.32/15.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 93.32/15.48
% 93.32/15.48
%------------------------------------------------------------------------------