%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL649+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n006.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 : Mon Sep 7 03:00:24 PM UTC 2026
% Result : CounterSatisfiable 0.23s 0.54s
% Output : Model 0.34s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff(p303_type,type,
p303: $i > $o ).
tff(p802_type,type,
p802: $i > $o ).
tff(p703_type,type,
p703: $i > $o ).
tff(p605_type,type,
p605: $i > $o ).
tff(p203_type,type,
p203: $i > $o ).
tff(p403_type,type,
p403: $i > $o ).
tff(p708_type,type,
p708: $i > $o ).
tff(p1109_type,type,
p1109: $i > $o ).
tff(p910_type,type,
p910: $i > $o ).
tff(p908_type,type,
p908: $i > $o ).
tff(p406_type,type,
p406: $i > $o ).
tff(p906_type,type,
p906: $i > $o ).
tff(p402_type,type,
p402: $i > $o ).
tff(p106_type,type,
p106: $i > $o ).
tff(p710_type,type,
p710: $i > $o ).
tff(p1006_type,type,
p1006: $i > $o ).
tff(p808_type,type,
p808: $i > $o ).
tff(p1104_type,type,
p1104: $i > $o ).
tff(p609_type,type,
p609: $i > $o ).
tff(p810_type,type,
p810: $i > $o ).
tff(p506_type,type,
p506: $i > $o ).
tff(p603_type,type,
p603: $i > $o ).
tff(p1107_type,type,
p1107: $i > $o ).
tff(p1007_type,type,
p1007: $i > $o ).
tff(p1002_type,type,
p1002: $i > $o ).
tff(p102_type,type,
p102: $i > $o ).
tff(p805_type,type,
p805: $i > $o ).
tff(p209_type,type,
p209: $i > $o ).
tff(p407_type,type,
p407: $i > $o ).
tff(p707_type,type,
p707: $i > $o ).
tff(p807_type,type,
p807: $i > $o ).
tff(p508_type,type,
p508: $i > $o ).
tff(p809_type,type,
p809: $i > $o ).
tff(p1110_type,type,
p1110: $i > $o ).
tff(p1009_type,type,
p1009: $i > $o ).
tff(p107_type,type,
p107: $i > $o ).
tff(p310_type,type,
p310: $i > $o ).
tff(p1010_type,type,
p1010: $i > $o ).
tff(p501_type,type,
p501: $i > $o ).
tff(p302_type,type,
p302: $i > $o ).
tff(p408_type,type,
p408: $i > $o ).
tff(p903_type,type,
p903: $i > $o ).
tff(p1103_type,type,
p1103: $i > $o ).
tff(p1102_type,type,
p1102: $i > $o ).
tff(p410_type,type,
p410: $i > $o ).
tff(p308_type,type,
p308: $i > $o ).
tff(p1001_type,type,
p1001: $i > $o ).
tff(p902_type,type,
p902: $i > $o ).
tff(p1004_type,type,
p1004: $i > $o ).
tff(p510_type,type,
p510: $i > $o ).
tff(p706_type,type,
p706: $i > $o ).
tff(p108_type,type,
p108: $i > $o ).
tff(p1108_type,type,
p1108: $i > $o ).
tff(p905_type,type,
p905: $i > $o ).
tff(p504_type,type,
p504: $i > $o ).
tff(p1003_type,type,
p1003: $i > $o ).
tff(p405_type,type,
p405: $i > $o ).
tff(p604_type,type,
p604: $i > $o ).
tff(p909_type,type,
p909: $i > $o ).
tff(p804_type,type,
p804: $i > $o ).
tff(p306_type,type,
p306: $i > $o ).
tff(p704_type,type,
p704: $i > $o ).
tff(p503_type,type,
p503: $i > $o ).
tff(p404_type,type,
p404: $i > $o ).
tff(p109_type,type,
p109: $i > $o ).
tff(p1106_type,type,
p1106: $i > $o ).
tff(p701_type,type,
p701: $i > $o ).
tff(p509_type,type,
p509: $i > $o ).
tff(p705_type,type,
p705: $i > $o ).
tff(p502_type,type,
p502: $i > $o ).
tff(p904_type,type,
p904: $i > $o ).
tff(p104_type,type,
p104: $i > $o ).
tff(p101_type,type,
p101: $i > $o ).
tff(p309_type,type,
p309: $i > $o ).
tff(p305_type,type,
p305: $i > $o ).
tff(p103_type,type,
p103: $i > $o ).
tff(p204_type,type,
p204: $i > $o ).
tff(p409_type,type,
p409: $i > $o ).
tff(p304_type,type,
p304: $i > $o ).
tff(p806_type,type,
p806: $i > $o ).
tff(p803_type,type,
p803: $i > $o ).
tff(p1005_type,type,
p1005: $i > $o ).
tff(p602_type,type,
p602: $i > $o ).
tff(p1008_type,type,
p1008: $i > $o ).
tff(p301_type,type,
p301: $i > $o ).
tff(p205_type,type,
p205: $i > $o ).
tff(p610_type,type,
p610: $i > $o ).
tff(p801_type,type,
p801: $i > $o ).
tff(p709_type,type,
p709: $i > $o ).
tff(p1105_type,type,
p1105: $i > $o ).
tff(p901_type,type,
p901: $i > $o ).
tff(r1_type,type,
r1: ( $i * $i ) > $o ).
tff(p606_type,type,
p606: $i > $o ).
tff(p505_type,type,
p505: $i > $o ).
tff(p202_type,type,
p202: $i > $o ).
tff(p702_type,type,
p702: $i > $o ).
tff(p207_type,type,
p207: $i > $o ).
tff(p206_type,type,
p206: $i > $o ).
tff(p607_type,type,
p607: $i > $o ).
tff(p907_type,type,
p907: $i > $o ).
tff(p1101_type,type,
p1101: $i > $o ).
tff(p401_type,type,
p401: $i > $o ).
tff(p601_type,type,
p601: $i > $o ).
tff(p201_type,type,
p201: $i > $o ).
tff(p608_type,type,
p608: $i > $o ).
tff(p208_type,type,
p208: $i > $o ).
tff(p210_type,type,
p210: $i > $o ).
tff(p507_type,type,
p507: $i > $o ).
tff(p307_type,type,
p307: $i > $o ).
tff(p110_type,type,
p110: $i > $o ).
tff(p105_type,type,
p105: $i > $o ).
tff(formula1,axiom,
! [X0: $i] :
( p303(X0)
<=> $true ) ).
tff(formula2,axiom,
! [X0: $i] :
( p802(X0)
<=> $false ) ).
tff(formula3,axiom,
! [X0: $i] :
( p703(X0)
<=> $false ) ).
tff(formula4,axiom,
! [X0: $i] :
( p605(X0)
<=> $false ) ).
tff(formula5,axiom,
! [X0: $i] :
( p203(X0)
<=> $false ) ).
tff(formula6,axiom,
! [X0: $i] :
( p403(X0)
<=> $false ) ).
tff(formula7,axiom,
! [X0: $i] :
( p708(X0)
<=> $false ) ).
tff(formula8,axiom,
! [X0: $i] :
( p1109(X0)
<=> $false ) ).
tff(formula9,axiom,
! [X0: $i] :
( p910(X0)
<=> $false ) ).
tff(formula10,axiom,
! [X0: $i] :
( p908(X0)
<=> $false ) ).
tff(formula11,axiom,
! [X0: $i] :
( p406(X0)
<=> $false ) ).
tff(formula12,axiom,
! [X0: $i] :
( p906(X0)
<=> $false ) ).
tff(formula13,axiom,
! [X0: $i] :
( p402(X0)
<=> $false ) ).
tff(formula14,axiom,
! [X0: $i] :
( p106(X0)
<=> $false ) ).
tff(formula15,axiom,
! [X0: $i] :
( p710(X0)
<=> $false ) ).
tff(formula16,axiom,
! [X0: $i] :
( p1006(X0)
<=> $false ) ).
tff(formula17,axiom,
! [X0: $i] :
( p808(X0)
<=> $true ) ).
tff(formula18,axiom,
! [X0: $i] :
( p1104(X0)
<=> $false ) ).
tff(formula19,axiom,
! [X0: $i] :
( p609(X0)
<=> $false ) ).
tff(formula20,axiom,
! [X0: $i] :
( p810(X0)
<=> $false ) ).
tff(formula21,axiom,
! [X0: $i] :
( p506(X0)
<=> $false ) ).
tff(formula22,axiom,
! [X0: $i] :
( p603(X0)
<=> $false ) ).
tff(formula23,axiom,
! [X0: $i] :
( p1107(X0)
<=> $false ) ).
tff(formula24,axiom,
! [X0: $i] :
( p1007(X0)
<=> $true ) ).
tff(formula25,axiom,
! [X0: $i] :
( p1002(X0)
<=> $false ) ).
tff(formula26,axiom,
! [X0: $i] :
( p102(X0)
<=> $false ) ).
tff(formula27,axiom,
! [X0: $i] :
( p805(X0)
<=> $false ) ).
tff(formula28,axiom,
! [X0: $i] :
( p209(X0)
<=> $false ) ).
tff(formula29,axiom,
! [X0: $i] :
( p407(X0)
<=> $false ) ).
tff(formula30,axiom,
! [X0: $i] :
( p707(X0)
<=> $true ) ).
tff(formula31,axiom,
! [X0: $i] :
( p807(X0)
<=> $false ) ).
tff(formula32,axiom,
! [X0: $i] :
( p508(X0)
<=> $false ) ).
tff(formula33,axiom,
! [X0: $i] :
( p809(X0)
<=> $false ) ).
tff(formula34,axiom,
! [X0: $i] :
( p1110(X0)
<=> $true ) ).
tff(formula35,axiom,
! [X0: $i] :
( p1009(X0)
<=> $false ) ).
tff(formula36,axiom,
! [X0: $i] :
( p107(X0)
<=> $false ) ).
tff(formula37,axiom,
! [X0: $i] :
( p310(X0)
<=> $false ) ).
tff(formula38,axiom,
! [X0: $i] :
( p1010(X0)
<=> $false ) ).
tff(formula39,axiom,
! [X0: $i] :
( p501(X0)
<=> $false ) ).
tff(formula40,axiom,
! [X0: $i] :
( p302(X0)
<=> $false ) ).
tff(formula41,axiom,
! [X0: $i] :
( p408(X0)
<=> $false ) ).
tff(formula42,axiom,
! [X0: $i] :
( p903(X0)
<=> $false ) ).
tff(formula43,axiom,
! [X0: $i] :
( p1103(X0)
<=> $false ) ).
tff(formula44,axiom,
! [X0: $i] :
( p1102(X0)
<=> $false ) ).
tff(formula45,axiom,
! [X0: $i] :
( p410(X0)
<=> $false ) ).
tff(formula46,axiom,
! [X0: $i] :
( p308(X0)
<=> $false ) ).
tff(formula47,axiom,
! [X0: $i] :
( p1001(X0)
<=> $false ) ).
tff(formula48,axiom,
! [X0: $i] :
( p902(X0)
<=> $false ) ).
tff(formula49,axiom,
! [X0: $i] :
( p1004(X0)
<=> $false ) ).
tff(formula50,axiom,
! [X0: $i] :
( p510(X0)
<=> $false ) ).
tff(formula51,axiom,
! [X0: $i] :
( p706(X0)
<=> $false ) ).
tff(formula52,axiom,
! [X0: $i] :
( p108(X0)
<=> $false ) ).
tff(formula53,axiom,
! [X0: $i] :
( p1108(X0)
<=> $false ) ).
tff(formula54,axiom,
! [X0: $i] :
( p905(X0)
<=> $false ) ).
tff(formula55,axiom,
! [X0: $i] :
( p504(X0)
<=> $false ) ).
tff(formula56,axiom,
! [X0: $i] :
( p1003(X0)
<=> $false ) ).
tff(formula57,axiom,
! [X0: $i] :
( p405(X0)
<=> $false ) ).
tff(formula58,axiom,
! [X0: $i] :
( p604(X0)
<=> $false ) ).
tff(formula59,axiom,
! [X0: $i] :
( p909(X0)
<=> $true ) ).
tff(formula60,axiom,
! [X0: $i] :
( p804(X0)
<=> $false ) ).
tff(formula61,axiom,
! [X0: $i] :
( p306(X0)
<=> $false ) ).
tff(formula62,axiom,
! [X0: $i] :
( p704(X0)
<=> $false ) ).
tff(formula63,axiom,
! [X0: $i] :
( p503(X0)
<=> $false ) ).
tff(formula64,axiom,
! [X0: $i] :
( p404(X0)
<=> $true ) ).
tff(formula65,axiom,
! [X0: $i] :
( p109(X0)
<=> $false ) ).
tff(formula66,axiom,
! [X0: $i] :
( p1106(X0)
<=> $false ) ).
tff(formula67,axiom,
! [X0: $i] :
( p701(X0)
<=> $false ) ).
tff(formula68,axiom,
! [X0: $i] :
( p509(X0)
<=> $false ) ).
tff(formula69,axiom,
! [X0: $i] :
( p705(X0)
<=> $false ) ).
tff(formula70,axiom,
! [X0: $i] :
( p502(X0)
<=> $false ) ).
tff(formula71,axiom,
! [X0: $i] :
( p904(X0)
<=> $false ) ).
tff(formula72,axiom,
! [X0: $i] :
( p104(X0)
<=> $false ) ).
tff(formula73,axiom,
! [X0: $i] :
( p101(X0)
<=> $true ) ).
tff(formula74,axiom,
! [X0: $i] :
( p309(X0)
<=> $false ) ).
tff(formula75,axiom,
! [X0: $i] :
( p305(X0)
<=> $false ) ).
tff(formula76,axiom,
! [X0: $i] :
( p103(X0)
<=> $false ) ).
tff(formula77,axiom,
! [X0: $i] :
( p204(X0)
<=> $false ) ).
tff(formula78,axiom,
! [X0: $i] :
( p409(X0)
<=> $false ) ).
tff(formula79,axiom,
! [X0: $i] :
( p304(X0)
<=> $false ) ).
tff(formula80,axiom,
! [X0: $i] :
( p806(X0)
<=> $false ) ).
tff(formula81,axiom,
! [X0: $i] :
( p803(X0)
<=> $false ) ).
tff(formula82,axiom,
! [X0: $i] :
( p1005(X0)
<=> $false ) ).
tff(formula83,axiom,
! [X0: $i] :
( p602(X0)
<=> $false ) ).
tff(formula84,axiom,
! [X0: $i] :
( p1008(X0)
<=> $false ) ).
tff(formula85,axiom,
! [X0: $i] :
( p301(X0)
<=> $false ) ).
tff(formula86,axiom,
! [X0: $i] :
( p205(X0)
<=> $false ) ).
tff(formula87,axiom,
! [X0: $i] :
( p610(X0)
<=> $false ) ).
tff(formula88,axiom,
! [X0: $i] :
( p801(X0)
<=> $false ) ).
tff(formula89,axiom,
! [X0: $i] :
( p709(X0)
<=> $false ) ).
tff(formula90,axiom,
! [X0: $i] :
( p1105(X0)
<=> $false ) ).
tff(formula91,axiom,
! [X0: $i] :
( p901(X0)
<=> $false ) ).
tff(formula92,axiom,
! [X0: $i,X1: $i] :
( r1(X0,X1)
<=> $true ) ).
tff(formula93,axiom,
! [X0: $i] :
( p606(X0)
<=> $true ) ).
tff(formula94,axiom,
! [X0: $i] :
( p505(X0)
<=> $true ) ).
tff(formula95,axiom,
! [X0: $i] :
( p202(X0)
<=> $true ) ).
tff(formula96,axiom,
! [X0: $i] :
( p702(X0)
<=> $false ) ).
tff(formula97,axiom,
! [X0: $i] :
( p207(X0)
<=> $false ) ).
tff(formula98,axiom,
! [X0: $i] :
( p206(X0)
<=> $false ) ).
tff(formula99,axiom,
! [X0: $i] :
( p607(X0)
<=> $false ) ).
tff(formula100,axiom,
! [X0: $i] :
( p907(X0)
<=> $false ) ).
tff(formula101,axiom,
! [X0: $i] :
( p1101(X0)
<=> $false ) ).
tff(formula102,axiom,
! [X0: $i] :
( p401(X0)
<=> $false ) ).
tff(formula103,axiom,
! [X0: $i] :
( p601(X0)
<=> $false ) ).
tff(formula104,axiom,
! [X0: $i] :
( p201(X0)
<=> $false ) ).
tff(formula105,axiom,
! [X0: $i] :
( p608(X0)
<=> $false ) ).
tff(formula106,axiom,
! [X0: $i] :
( p208(X0)
<=> $false ) ).
tff(formula107,axiom,
! [X0: $i] :
( p210(X0)
<=> $false ) ).
tff(formula108,axiom,
! [X0: $i] :
( p507(X0)
<=> $false ) ).
tff(formula109,axiom,
! [X0: $i] :
( p307(X0)
<=> $false ) ).
tff(formula110,axiom,
! [X0: $i] :
( p110(X0)
<=> $false ) ).
tff(formula111,axiom,
! [X0: $i] :
( p105(X0)
<=> $false ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL649+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 08:10:03 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.23/0.54 % SZS status CounterSatisfiable
% 0.23/0.54 % SZS output start Model
% See solution above
% 0.34/0.57 % E exiting
%------------------------------------------------------------------------------