%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ135_2 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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:33:02 PM UTC 2026
% Result : Theorem 2.03s 1.28s
% Output : CNFRefutation 2.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 21
% Syntax : Number of formulae : 165 ( 43 unt; 0 typ; 0 def)
% Number of atoms : 465 ( 464 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 506 ( 206 ~; 272 |; 22 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-1 aty)
% Number of variables : 97 ( 0 sgn 97 !; 0 ?; 97 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
entry_of: knowheyan > entry ).
tff(func_def_1,type,
place_of: knowheyan > place ).
tff(func_def_2,type,
a: knowheyan ).
tff(func_def_3,type,
b: knowheyan ).
tff(func_def_4,type,
c: knowheyan ).
tff(func_def_5,type,
d: knowheyan ).
tff(func_def_6,type,
collage_painting: entry ).
tff(func_def_7,type,
holography: entry ).
tff(func_def_8,type,
laser_etching: entry ).
tff(func_def_9,type,
reconstituted_materials_sculpture: entry ).
tff(func_def_10,type,
first: place ).
tff(func_def_11,type,
second: place ).
tff(func_def_12,type,
third: place ).
tff(func_def_13,type,
fourth: place ).
tff(f1,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_b) ).
tff(f2,axiom,
a != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_c) ).
tff(f3,axiom,
a != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_d) ).
tff(f4,axiom,
b != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_not_c) ).
tff(f5,axiom,
b != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_not_d) ).
tff(f6,axiom,
c != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_not_d) ).
tff(f19,axiom,
! [X0: knowheyan] :
( ( X0 = d )
| ( X0 = c )
| ( X0 = b )
| ( X0 = a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',only_knowheyans) ).
tff(f20,axiom,
! [X0: entry] :
( ( X0 = reconstituted_materials_sculpture )
| ( X0 = laser_etching )
| ( X0 = holography )
| ( X0 = collage_painting ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',only_entries) ).
tff(f21,axiom,
! [X0: place] :
( ( X0 = fourth )
| ( X0 = third )
| ( X0 = second )
| ( X0 = first ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',only_places) ).
tff(f22,axiom,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 != X1 )
=> ( entry_of(X0) != entry_of(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_entrys) ).
tff(f23,axiom,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 != X1 )
=> ( place_of(X0) != place_of(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_places) ).
tff(f24,axiom,
( ( entry_of(a) != holography )
& ( place_of(a) != first ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_info) ).
tff(f25,axiom,
! [X0: knowheyan] :
( ( place_of(X0) = fourth )
=> ( ( entry_of(X0) != holography )
& ( entry_of(X0) != reconstituted_materials_sculpture ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fourth_info) ).
tff(f26,axiom,
! [X0: knowheyan] :
( ( entry_of(X0) = collage_painting )
=> ( ( place_of(X0) != second )
& ( place_of(X0) != first )
& ( X0 != c )
& ( X0 != a ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',collage_info) ).
tff(f27,axiom,
( ! [X0: knowheyan] :
( ( entry_of(X0) = laser_etching )
=> ( place_of(X0) != fourth ) )
& ( place_of(b) != fourth ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fourth_info2) ).
tff(f28,axiom,
( ( place_of(c) != third )
& ( place_of(b) != third ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',third_info) ).
tff(f29,axiom,
( ! [X0: knowheyan] :
( ( entry_of(X0) = laser_etching )
=> ( ( place_of(X0) != second )
& ( X0 != a ) ) )
& ( entry_of(b) != laser_etching ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',laser_etching_info) ).
tff(f30,conjecture,
( ( place_of(d) = fourth )
& ( place_of(c) = first )
& ( place_of(b) = second )
& ( place_of(a) = third ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',places) ).
tff(f31,negated_conjecture,
~ ( ( place_of(d) = fourth )
& ( place_of(c) = first )
& ( place_of(b) = second )
& ( place_of(a) = third ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
tff(f32,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 = X1 )
| ( entry_of(X0) != entry_of(X1) ) ),
inference(ennf_transformation,[],[f22]) ).
tff(f33,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 = X1 )
| ( place_of(X0) != place_of(X1) ) ),
inference(ennf_transformation,[],[f23]) ).
tff(f34,plain,
! [X0: knowheyan] :
( ( fourth != place_of(X0) )
| ( ( entry_of(X0) != holography )
& ( entry_of(X0) != reconstituted_materials_sculpture ) ) ),
inference(ennf_transformation,[],[f25]) ).
tff(f35,plain,
! [X0: knowheyan] :
( ( collage_painting != entry_of(X0) )
| ( ( place_of(X0) != second )
& ( place_of(X0) != first )
& ( X0 != c )
& ( X0 != a ) ) ),
inference(ennf_transformation,[],[f26]) ).
tff(f36,plain,
( ! [X0: knowheyan] :
( ( laser_etching != entry_of(X0) )
| ( place_of(X0) != fourth ) )
& ( place_of(b) != fourth ) ),
inference(ennf_transformation,[],[f27]) ).
tff(f37,plain,
( ! [X0: knowheyan] :
( ( laser_etching != entry_of(X0) )
| ( ( place_of(X0) != second )
& ( X0 != a ) ) )
& ( entry_of(b) != laser_etching ) ),
inference(ennf_transformation,[],[f29]) ).
tff(f38,plain,
( ( fourth != place_of(d) )
| ( first != place_of(c) )
| ( second != place_of(b) )
| ( third != place_of(a) ) ),
inference(ennf_transformation,[],[f31]) ).
tff(f39,plain,
a != b,
inference(cnf_transformation,[],[f1]) ).
tff(f40,plain,
a != c,
inference(cnf_transformation,[],[f2]) ).
tff(f41,plain,
a != d,
inference(cnf_transformation,[],[f3]) ).
tff(f42,plain,
b != c,
inference(cnf_transformation,[],[f4]) ).
tff(f43,plain,
b != d,
inference(cnf_transformation,[],[f5]) ).
tff(f44,plain,
c != d,
inference(cnf_transformation,[],[f6]) ).
tff(f57,plain,
! [X0: knowheyan] :
( ( d = X0 )
| ( c = X0 )
| ( b = X0 )
| ( a = X0 ) ),
inference(cnf_transformation,[],[f19]) ).
tff(f58,plain,
! [X0: entry] :
( ( reconstituted_materials_sculpture = X0 )
| ( laser_etching = X0 )
| ( holography = X0 )
| ( collage_painting = X0 ) ),
inference(cnf_transformation,[],[f20]) ).
tff(f59,plain,
! [X0: place] :
( ( fourth = X0 )
| ( third = X0 )
| ( second = X0 )
| ( first = X0 ) ),
inference(cnf_transformation,[],[f21]) ).
tff(f60,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 = X1 )
| ( entry_of(X0) != entry_of(X1) ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f61,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 = X1 )
| ( place_of(X0) != place_of(X1) ) ),
inference(cnf_transformation,[],[f33]) ).
tff(f62,plain,
holography != entry_of(a),
inference(cnf_transformation,[],[f24]) ).
tff(f63,plain,
first != place_of(a),
inference(cnf_transformation,[],[f24]) ).
tff(f65,plain,
! [X0: knowheyan] :
( ( fourth != place_of(X0) )
| ( reconstituted_materials_sculpture != entry_of(X0) ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f66,plain,
! [X0: knowheyan] :
( ( collage_painting != entry_of(X0) )
| ( second != place_of(X0) ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f67,plain,
! [X0: knowheyan] :
( ( collage_painting != entry_of(X0) )
| ( first != place_of(X0) ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f68,plain,
! [X0: knowheyan] :
( ( collage_painting != entry_of(X0) )
| ( c != X0 ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f69,plain,
! [X0: knowheyan] :
( ( collage_painting != entry_of(X0) )
| ( a != X0 ) ),
inference(cnf_transformation,[],[f35]) ).
tff(f70,plain,
! [X0: knowheyan] :
( ( laser_etching != entry_of(X0) )
| ( fourth != place_of(X0) ) ),
inference(cnf_transformation,[],[f36]) ).
tff(f71,plain,
fourth != place_of(b),
inference(cnf_transformation,[],[f36]) ).
tff(f72,plain,
third != place_of(c),
inference(cnf_transformation,[],[f28]) ).
tff(f73,plain,
third != place_of(b),
inference(cnf_transformation,[],[f28]) ).
tff(f74,plain,
! [X0: knowheyan] :
( ( laser_etching != entry_of(X0) )
| ( second != place_of(X0) ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f75,plain,
! [X0: knowheyan] :
( ( laser_etching != entry_of(X0) )
| ( a != X0 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f76,plain,
laser_etching != entry_of(b),
inference(cnf_transformation,[],[f37]) ).
tff(f77,plain,
( ( fourth != place_of(d) )
| ( first != place_of(c) )
| ( second != place_of(b) )
| ( third != place_of(a) ) ),
inference(cnf_transformation,[],[f38]) ).
tff(f78,plain,
collage_painting != entry_of(a),
inference(equality_resolution,[],[f69]) ).
tff(f79,plain,
collage_painting != entry_of(c),
inference(equality_resolution,[],[f68]) ).
tff(f80,plain,
laser_etching != entry_of(a),
inference(equality_resolution,[],[f75]) ).
tcf(c_49,plain,
a != b,
inference(cnf_transformation,[],[f39]) ).
tcf(c_50,plain,
a != c,
inference(cnf_transformation,[],[f40]) ).
tcf(c_51,plain,
a != d,
inference(cnf_transformation,[],[f41]) ).
tcf(c_52,plain,
b != c,
inference(cnf_transformation,[],[f42]) ).
tcf(c_53,plain,
b != d,
inference(cnf_transformation,[],[f43]) ).
tcf(c_54,plain,
c != d,
inference(cnf_transformation,[],[f44]) ).
tcf(c_67,plain,
! [X0_knowheyan: knowheyan] :
( ( X0_knowheyan = d )
| ( X0_knowheyan = c )
| ( X0_knowheyan = b )
| ( X0_knowheyan = a ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_68,plain,
! [X0_entry: entry] :
( ( X0_entry = reconstituted_materials_sculpture )
| ( X0_entry = laser_etching )
| ( X0_entry = holography )
| ( X0_entry = collage_painting ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_69,plain,
! [X0_place: place] :
( ( X0_place = fourth )
| ( X0_place = third )
| ( X0_place = second )
| ( X0_place = first ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_70,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan] :
( ( X0_knowheyan = X1_knowheyan )
| ( entry_of(X0_knowheyan) != entry_of(X1_knowheyan) ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_71,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan] :
( ( X0_knowheyan = X1_knowheyan )
| ( place_of(X0_knowheyan) != place_of(X1_knowheyan) ) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_72,plain,
place_of(a) != first,
inference(cnf_transformation,[],[f63]) ).
tcf(c_73,plain,
entry_of(a) != holography,
inference(cnf_transformation,[],[f62]) ).
tcf(c_74,plain,
! [X0_knowheyan: knowheyan] :
( ( place_of(X0_knowheyan) != fourth )
| ( entry_of(X0_knowheyan) != reconstituted_materials_sculpture ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_76,plain,
entry_of(a) != collage_painting,
inference(cnf_transformation,[],[f78]) ).
tcf(c_77,plain,
entry_of(c) != collage_painting,
inference(cnf_transformation,[],[f79]) ).
tcf(c_78,plain,
! [X0_knowheyan: knowheyan] :
( ( place_of(X0_knowheyan) != first )
| ( entry_of(X0_knowheyan) != collage_painting ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_79,plain,
! [X0_knowheyan: knowheyan] :
( ( place_of(X0_knowheyan) != second )
| ( entry_of(X0_knowheyan) != collage_painting ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_80,plain,
place_of(b) != fourth,
inference(cnf_transformation,[],[f71]) ).
tcf(c_81,plain,
! [X0_knowheyan: knowheyan] :
( ( place_of(X0_knowheyan) != fourth )
| ( entry_of(X0_knowheyan) != laser_etching ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_82,plain,
place_of(b) != third,
inference(cnf_transformation,[],[f73]) ).
tcf(c_83,plain,
place_of(c) != third,
inference(cnf_transformation,[],[f72]) ).
tcf(c_84,plain,
entry_of(b) != laser_etching,
inference(cnf_transformation,[],[f76]) ).
tcf(c_85,plain,
entry_of(a) != laser_etching,
inference(cnf_transformation,[],[f80]) ).
tcf(c_86,plain,
! [X0_knowheyan: knowheyan] :
( ( place_of(X0_knowheyan) != second )
| ( entry_of(X0_knowheyan) != laser_etching ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_87,negated_conjecture,
( ( place_of(d) != fourth )
| ( place_of(c) != first )
| ( place_of(b) != second )
| ( place_of(a) != third ) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_90,plain,
( ( place_of(a) != fourth )
| ( entry_of(a) != reconstituted_materials_sculpture ) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_93,plain,
( ( a = d )
| ( a = c )
| ( a = b )
| ( a = a ) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_223,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan,X2_knowheyan: knowheyan] :
( ( X2_knowheyan = X0_knowheyan )
| ( X2_knowheyan != X1_knowheyan )
| ( X0_knowheyan != X1_knowheyan ) ),
theory(equality) ).
tcf(c_224,plain,
! [X0_place: place,X1_place: place,X2_place: place] :
( ( X2_place = X0_place )
| ( X2_place != X1_place )
| ( X0_place != X1_place ) ),
theory(equality) ).
tcf(c_225,plain,
! [X0_entry: entry,X1_entry: entry,X2_entry: entry] :
( ( X2_entry = X0_entry )
| ( X2_entry != X1_entry )
| ( X0_entry != X1_entry ) ),
theory(equality) ).
tcf(c_518,plain,
entry_of(a) != entry_of(b),
inference(resolution,[status(thm)],[c_70,c_49]) ).
tcf(c_520,plain,
entry_of(a) != entry_of(d),
inference(resolution,[status(thm)],[c_70,c_51]) ).
tcf(c_522,plain,
entry_of(b) != entry_of(d),
inference(resolution,[status(thm)],[c_70,c_53]) ).
tcf(c_523,plain,
entry_of(c) != entry_of(d),
inference(resolution,[status(thm)],[c_70,c_54]) ).
tcf(c_535,plain,
place_of(b) != place_of(c),
inference(resolution,[status(thm)],[c_71,c_52]) ).
tcf(c_537,plain,
place_of(c) != place_of(d),
inference(resolution,[status(thm)],[c_71,c_54]) ).
tcf(c_579,plain,
! [X0_knowheyan: knowheyan] :
( ( d != X0_knowheyan )
| ( a != X0_knowheyan ) ),
inference(resolution,[status(thm)],[c_223,c_51]) ).
tcf(c_587,plain,
( ( entry_of(a) = reconstituted_materials_sculpture )
| ( entry_of(a) = laser_etching )
| ( entry_of(a) = holography )
| ( entry_of(a) = collage_painting ) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_589,plain,
! [X0_knowheyan: knowheyan] :
( ( entry_of(X0_knowheyan) = reconstituted_materials_sculpture )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = holography )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_598,plain,
( ( place_of(a) = fourth )
| ( place_of(a) = third )
| ( place_of(a) = second )
| ( place_of(a) = first ) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_615,plain,
! [X0_knowheyan: knowheyan] :
( ( a != X0_knowheyan )
| ( place_of(d) != place_of(X0_knowheyan) ) ),
inference(resolution,[status(thm)],[c_579,c_71]) ).
tcf(c_618,plain,
( ( a != a )
| ( place_of(d) != place_of(a) ) ),
inference(instantiation,[status(thm)],[c_615]) ).
tcf(c_668,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan] :
( ( X0_knowheyan = X1_knowheyan )
| ( entry_of(X1_knowheyan) = laser_etching )
| ( entry_of(X1_knowheyan) = holography )
| ( entry_of(X1_knowheyan) = collage_painting )
| ( entry_of(X0_knowheyan) != reconstituted_materials_sculpture ) ),
inference(superposition,[status(thm)],[c_68,c_70]) ).
tcf(c_669,plain,
! [X0_entry: entry,X1_entry: entry] :
( ( X1_entry = laser_etching )
| ( X1_entry = holography )
| ( X1_entry = collage_painting )
| ( X0_entry = laser_etching )
| ( X0_entry = holography )
| ( X0_entry = collage_painting )
| ( X0_entry = X1_entry ) ),
inference(superposition,[status(thm)],[c_68,c_68]) ).
tcf(c_742,plain,
! [X0_place: place] :
( ( place_of(d) != X0_place )
| ( place_of(c) != X0_place ) ),
inference(resolution,[status(thm)],[c_224,c_537]) ).
tcf(c_743,plain,
( ( place_of(d) != fourth )
| ( place_of(c) != fourth ) ),
inference(instantiation,[status(thm)],[c_742]) ).
tcf(c_759,plain,
( ( place_of(c) = fourth )
| ( place_of(c) = second )
| ( place_of(c) = first ) ),
inference(superposition,[status(thm)],[c_69,c_83]) ).
tcf(c_761,plain,
( ( place_of(b) = fourth )
| ( place_of(b) = second )
| ( place_of(b) = first ) ),
inference(superposition,[status(thm)],[c_69,c_82]) ).
tcf(c_793,plain,
( ( place_of(b) = first )
| ( place_of(b) = second ) ),
inference(global_subsumption_just,[status(thm)],[c_761,c_80,c_761]) ).
tcf(c_794,plain,
( ( place_of(b) = second )
| ( place_of(b) = first ) ),
inference(renaming,[status(thm)],[c_793]) ).
tcf(c_799,plain,
! [X0_knowheyan: knowheyan] :
( ( X0_knowheyan = b )
| ( place_of(b) = first )
| ( place_of(X0_knowheyan) != second ) ),
inference(superposition,[status(thm)],[c_794,c_71]) ).
tcf(c_803,plain,
( ( a = b )
| ( place_of(b) = first )
| ( place_of(a) != second ) ),
inference(instantiation,[status(thm)],[c_799]) ).
tcf(c_806,plain,
( ( b = c )
| ( place_of(c) = fourth )
| ( place_of(c) = first )
| ( place_of(b) = first ) ),
inference(superposition,[status(thm)],[c_759,c_799]) ).
tcf(c_811,plain,
( ( place_of(b) = first )
| ( place_of(c) = first )
| ( place_of(c) = fourth ) ),
inference(global_subsumption_just,[status(thm)],[c_806,c_52,c_806]) ).
tcf(c_812,plain,
( ( place_of(c) = fourth )
| ( place_of(c) = first )
| ( place_of(b) = first ) ),
inference(renaming,[status(thm)],[c_811]) ).
tcf(c_824,plain,
( ( place_of(c) = fourth )
| ( place_of(b) = first )
| ( place_of(d) != fourth )
| ( place_of(b) != second )
| ( place_of(a) != third ) ),
inference(superposition,[status(thm)],[c_812,c_87]) ).
tcf(c_877,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan] :
( ( X0_knowheyan = X1_knowheyan )
| ( entry_of(X1_knowheyan) = laser_etching )
| ( entry_of(X1_knowheyan) = holography )
| ( entry_of(X1_knowheyan) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = holography )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(superposition,[status(thm)],[c_68,c_668]) ).
tcf(c_882,plain,
( ( place_of(d) != fourth )
| ( place_of(b) = first ) ),
inference(global_subsumption_just,[status(thm)],[c_824,c_49,c_85,c_76,c_73,c_72,c_90,c_587,c_598,c_743,c_794,c_803,c_824]) ).
tcf(c_883,plain,
( ( place_of(b) = first )
| ( place_of(d) != fourth ) ),
inference(renaming,[status(thm)],[c_882]) ).
tcf(c_1035,plain,
( ( place_of(d) = fourth )
| ( place_of(d) = third )
| ( place_of(d) = second )
| ( place_of(d) = first ) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_1041,plain,
! [X0_place: place,X1_place: place] :
( ( place_of(d) = X1_place )
| ( X1_place != X0_place )
| ( place_of(d) != X0_place ) ),
inference(instantiation,[status(thm)],[c_224]) ).
tcf(c_1096,plain,
! [X0_entry: entry] :
( ( X0_entry = laser_etching )
| ( X0_entry = holography )
| ( X0_entry = collage_painting )
| ( entry_of(a) = laser_etching )
| ( entry_of(a) = collage_painting )
| ( entry_of(a) = X0_entry ) ),
inference(superposition,[status(thm)],[c_669,c_73]) ).
tcf(c_1183,plain,
! [X0_entry: entry] :
( ( entry_of(a) = entry_of(b) )
| ( entry_of(b) != X0_entry )
| ( entry_of(a) != X0_entry ) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1201,plain,
! [X0_entry: entry] :
( ( entry_of(a) = entry_of(d) )
| ( entry_of(d) != X0_entry )
| ( entry_of(a) != X0_entry ) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1204,plain,
! [X0_entry: entry] :
( ( X0_entry = laser_etching )
| ( X0_entry = holography )
| ( X0_entry = collage_painting )
| ( entry_of(a) = X0_entry ) ),
inference(global_subsumption_just,[status(thm)],[c_1096,c_85,c_76,c_1096]) ).
tcf(c_1218,plain,
! [X0_knowheyan: knowheyan,X0_entry: entry] :
( ( X0_entry = laser_etching )
| ( X0_entry = holography )
| ( X0_entry = collage_painting )
| ( X0_knowheyan = a )
| ( entry_of(X0_knowheyan) != X0_entry ) ),
inference(superposition,[status(thm)],[c_1204,c_70]) ).
tcf(c_1242,plain,
! [X0_entry: entry] :
( ( entry_of(b) = entry_of(d) )
| ( entry_of(d) != X0_entry )
| ( entry_of(b) != X0_entry ) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1243,plain,
( ( entry_of(b) = entry_of(d) )
| ( entry_of(d) != collage_painting )
| ( entry_of(b) != collage_painting ) ),
inference(instantiation,[status(thm)],[c_1242]) ).
tcf(c_1249,plain,
! [X0_entry: entry] :
( ( entry_of(c) = entry_of(d) )
| ( entry_of(d) != X0_entry )
| ( entry_of(c) != X0_entry ) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_1286,plain,
! [X0_place: place] :
( ( place_of(c) = place_of(d) )
| ( place_of(d) != X0_place )
| ( place_of(c) != X0_place ) ),
inference(instantiation,[status(thm)],[c_224]) ).
tcf(c_1315,plain,
! [X0_knowheyan: knowheyan] :
( ( X0_knowheyan = a )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = holography )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(equality_resolution,[status(thm)],[c_1218]) ).
tcf(c_1610,plain,
! [X0_knowheyan: knowheyan] :
( ( entry_of(d) = laser_etching )
| ( entry_of(d) = holography )
| ( entry_of(d) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = holography )
| ( entry_of(X0_knowheyan) = collage_painting )
| ( X0_knowheyan != a ) ),
inference(superposition,[status(thm)],[c_877,c_51]) ).
tcf(c_1612,plain,
! [X0_knowheyan: knowheyan] :
( ( entry_of(c) = laser_etching )
| ( entry_of(c) = holography )
| ( entry_of(c) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = holography )
| ( entry_of(X0_knowheyan) = collage_painting )
| ( X0_knowheyan != a ) ),
inference(superposition,[status(thm)],[c_877,c_50]) ).
tcf(c_1613,plain,
! [X0_knowheyan: knowheyan] :
( ( entry_of(c) = laser_etching )
| ( entry_of(c) = holography )
| ( entry_of(c) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = holography )
| ( entry_of(X0_knowheyan) = collage_painting )
| ( place_of(d) != fourth )
| ( place_of(b) != second )
| ( place_of(a) != third )
| ( place_of(X0_knowheyan) != first ) ),
inference(superposition,[status(thm)],[c_877,c_87]) ).
tcf(c_1618,plain,
( ( entry_of(c) = laser_etching )
| ( entry_of(c) = holography )
| ( entry_of(c) = collage_painting )
| ( entry_of(a) = laser_etching )
| ( entry_of(a) = holography )
| ( entry_of(a) = collage_painting )
| ( a != a ) ),
inference(instantiation,[status(thm)],[c_1612]) ).
tcf(c_1619,plain,
( ( entry_of(d) = laser_etching )
| ( entry_of(d) = holography )
| ( entry_of(d) = collage_painting )
| ( entry_of(a) = laser_etching )
| ( entry_of(a) = holography )
| ( entry_of(a) = collage_painting )
| ( a != a ) ),
inference(instantiation,[status(thm)],[c_1610]) ).
tcf(c_1632,plain,
( ( entry_of(c) = laser_etching )
| ( entry_of(c) = holography ) ),
inference(global_subsumption_just,[status(thm)],[c_1613,c_51,c_50,c_49,c_85,c_77,c_76,c_73,c_93,c_1618]) ).
tcf(c_1704,plain,
! [X0_knowheyan: knowheyan] :
( ( X0_knowheyan = c )
| ( entry_of(c) = laser_etching )
| ( entry_of(X0_knowheyan) != holography ) ),
inference(superposition,[status(thm)],[c_1632,c_70]) ).
tcf(c_1708,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan] :
( ( X0_knowheyan = c )
| ( X0_knowheyan = X1_knowheyan )
| ( entry_of(c) = laser_etching )
| ( entry_of(X1_knowheyan) = laser_etching )
| ( entry_of(X1_knowheyan) = holography )
| ( entry_of(X1_knowheyan) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(superposition,[status(thm)],[c_877,c_1704]) ).
tcf(c_1783,plain,
! [X0_knowheyan: knowheyan,X1_knowheyan: knowheyan] :
( ( X1_knowheyan = c )
| ( X0_knowheyan = c )
| ( X0_knowheyan = X1_knowheyan )
| ( entry_of(c) = laser_etching )
| ( entry_of(X1_knowheyan) = laser_etching )
| ( entry_of(X1_knowheyan) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(superposition,[status(thm)],[c_1708,c_1704]) ).
tcf(c_1845,plain,
! [X0_place: place,X1_place: place] :
( ( place_of(b) = X1_place )
| ( X1_place != X0_place )
| ( place_of(b) != X0_place ) ),
inference(instantiation,[status(thm)],[c_224]) ).
tcf(c_1953,plain,
! [X0_knowheyan: knowheyan] :
( ( c = d )
| ( X0_knowheyan = c )
| ( entry_of(d) = laser_etching )
| ( entry_of(d) = collage_painting )
| ( entry_of(c) = laser_etching )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting )
| ( X0_knowheyan != b ) ),
inference(superposition,[status(thm)],[c_1783,c_53]) ).
tcf(c_1999,plain,
! [X0_knowheyan: knowheyan] :
( ( a = c )
| ( X0_knowheyan = c )
| ( X0_knowheyan = a )
| ( entry_of(c) = laser_etching )
| ( entry_of(a) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(superposition,[status(thm)],[c_1783,c_85]) ).
tcf(c_2005,plain,
! [X0_knowheyan: knowheyan] :
( ( b = c )
| ( X0_knowheyan = c )
| ( X0_knowheyan = b )
| ( entry_of(c) = laser_etching )
| ( entry_of(b) = collage_painting )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(superposition,[status(thm)],[c_1783,c_84]) ).
tcf(c_2265,plain,
( ( entry_of(a) = entry_of(b) )
| ( entry_of(b) != reconstituted_materials_sculpture )
| ( entry_of(a) != reconstituted_materials_sculpture ) ),
inference(instantiation,[status(thm)],[c_1183]) ).
tcf(c_2267,plain,
( ( entry_of(b) = reconstituted_materials_sculpture )
| ( entry_of(b) = laser_etching )
| ( entry_of(b) = holography )
| ( entry_of(b) = collage_painting ) ),
inference(instantiation,[status(thm)],[c_589]) ).
tcf(c_2280,plain,
! [X0_knowheyan: knowheyan] :
( ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting )
| ( entry_of(c) = laser_etching )
| ( X0_knowheyan = a )
| ( X0_knowheyan = c ) ),
inference(global_subsumption_just,[status(thm)],[c_1999,c_1315,c_1704]) ).
tcf(c_2281,plain,
! [X0_knowheyan: knowheyan] :
( ( X0_knowheyan = c )
| ( X0_knowheyan = a )
| ( entry_of(c) = laser_etching )
| ( entry_of(X0_knowheyan) = laser_etching )
| ( entry_of(X0_knowheyan) = collage_painting ) ),
inference(renaming,[status(thm)],[c_2280]) ).
tcf(c_2321,plain,
( ( b = c )
| ( a = b )
| ( entry_of(c) = laser_etching )
| ( entry_of(b) = collage_painting ) ),
inference(superposition,[status(thm)],[c_2281,c_84]) ).
tcf(c_2337,plain,
( ( entry_of(a) = entry_of(d) )
| ( entry_of(d) != reconstituted_materials_sculpture )
| ( entry_of(a) != reconstituted_materials_sculpture ) ),
inference(instantiation,[status(thm)],[c_1201]) ).
tcf(c_2408,plain,
( ( entry_of(c) = entry_of(d) )
| ( entry_of(d) != holography )
| ( entry_of(c) != holography ) ),
inference(instantiation,[status(thm)],[c_1249]) ).
tcf(c_2482,plain,
( ( entry_of(b) = collage_painting )
| ( entry_of(c) = laser_etching ) ),
inference(global_subsumption_just,[status(thm)],[c_2005,c_52,c_49,c_2321]) ).
tcf(c_2483,plain,
( ( entry_of(c) = laser_etching )
| ( entry_of(b) = collage_painting ) ),
inference(renaming,[status(thm)],[c_2482]) ).
tcf(c_2545,plain,
! [X0_knowheyan: knowheyan,X0_place: place] :
( ( place_of(d) = place_of(X0_knowheyan) )
| ( place_of(d) != X0_place )
| ( place_of(X0_knowheyan) != X0_place ) ),
inference(instantiation,[status(thm)],[c_1041]) ).
tcf(c_2754,plain,
( ( entry_of(d) = laser_etching )
| ( entry_of(c) = laser_etching ) ),
inference(global_subsumption_just,[status(thm)],[c_1953,c_51,c_50,c_49,c_85,c_76,c_73,c_93,c_522,c_523,c_1243,c_1619,c_1632,c_2408,c_2483]) ).
tcf(c_2789,plain,
! [X0_place: place] :
( ( place_of(b) = X0_place )
| ( X0_place != first )
| ( place_of(b) != first ) ),
inference(instantiation,[status(thm)],[c_1845]) ).
tcf(c_2892,plain,
( ( entry_of(d) = reconstituted_materials_sculpture )
| ( entry_of(d) = laser_etching )
| ( entry_of(d) = holography )
| ( entry_of(d) = collage_painting ) ),
inference(instantiation,[status(thm)],[c_589]) ).
tcf(c_2968,plain,
( ( entry_of(b) = entry_of(d) )
| ( entry_of(d) != holography )
| ( entry_of(b) != holography ) ),
inference(instantiation,[status(thm)],[c_1242]) ).
tcf(c_4403,plain,
( ( place_of(c) != second )
| ( entry_of(c) != laser_etching ) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_4404,plain,
( ( place_of(c) != fourth )
| ( entry_of(c) != laser_etching ) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_4408,plain,
( ( entry_of(c) = entry_of(d) )
| ( entry_of(d) != laser_etching )
| ( entry_of(c) != laser_etching ) ),
inference(instantiation,[status(thm)],[c_1249]) ).
tcf(c_4600,plain,
( ( place_of(d) != second )
| ( entry_of(d) != collage_painting ) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_4664,plain,
( ( place_of(b) = place_of(c) )
| ( place_of(c) != first )
| ( place_of(b) != first ) ),
inference(instantiation,[status(thm)],[c_2789]) ).
tcf(c_4666,plain,
( ( place_of(c) = place_of(d) )
| ( place_of(d) != first )
| ( place_of(c) != first ) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_5983,plain,
! [X0_knowheyan: knowheyan] :
( ( place_of(d) = place_of(X0_knowheyan) )
| ( place_of(d) != third )
| ( place_of(X0_knowheyan) != third ) ),
inference(instantiation,[status(thm)],[c_2545]) ).
tcf(c_5985,plain,
( ( place_of(d) = place_of(a) )
| ( place_of(d) != third )
| ( place_of(a) != third ) ),
inference(instantiation,[status(thm)],[c_5983]) ).
tcf(c_6113,plain,
( ( place_of(b) != second )
| ( entry_of(b) != collage_painting ) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_6114,plain,
( ( place_of(b) != first )
| ( entry_of(b) != collage_painting ) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_6912,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_6113,c_6114,c_5985,c_4666,c_4664,c_4600,c_4408,c_4403,c_4404,c_2968,c_2892,c_2754,c_2483,c_2337,c_2267,c_2265,c_1035,c_883,c_803,c_794,c_759,c_618,c_598,c_587,c_537,c_535,c_523,c_522,c_520,c_518,c_93,c_90,c_72,c_73,c_76,c_84,c_85,c_49,c_50,c_51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ135_2 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n014.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 : Thu Sep 24 07:01:02 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/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...
% 2.03/1.28 % SZS status Started for theBenchmark.p
% 2.03/1.28 % SZS status Theorem for theBenchmark.p
% 2.03/1.28
% 2.03/1.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.03/1.28
% 2.03/1.28 % ------ iProver source info
% 2.03/1.28
% 2.03/1.28 % git: date: 2026-07-19 20:42:38 +0200
% 2.03/1.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.03/1.28 % git: non_committed_changes: false
% 2.03/1.28
% 2.03/1.28 % ------ Parsing...
% 2.03/1.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.03/1.28
% 2.03/1.28 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.03/1.28
% 2.03/1.28 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.03/1.28
% 2.03/1.28 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 2.03/1.28 % ------ Proving...
% 2.03/1.28 % ------ Problem Properties
% 2.03/1.28
% 2.03/1.28 %
% 2.03/1.28 % clauses 39
% 2.03/1.28 % conjectures 1
% 2.03/1.28 % EPR 21
% 2.03/1.28 % Horn 36
% 2.03/1.28 % unary 27
% 2.03/1.28 % binary 8
% 2.03/1.28 % lits 59
% 2.03/1.28 % lits eq 59
% 2.03/1.28 % fd_pure 3
% 2.03/1.28 % fd_pseudo 0
% 2.03/1.28 % fd_cond 0
% 2.03/1.28 % fd_pseudo_cond 2
% 2.03/1.28 % AC symbols 0
% 2.03/1.28
% 2.03/1.28 % ------ Input Options Time Limit: Unbounded
% 2.03/1.28
% 2.03/1.28
% 2.03/1.28 % ------
% 2.03/1.28 % Current options:
% 2.03/1.28 % ------
% 2.03/1.28
% 2.03/1.28
% 2.03/1.28 %
% 2.03/1.28
% 2.03/1.28 % ------ Proving...
% 2.03/1.28 %
% 2.03/1.28
% 2.03/1.28 % SZS status Theorem for theBenchmark.p
% 2.03/1.28
% 2.03/1.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.03/1.29
% 2.03/1.29
%------------------------------------------------------------------------------