%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN538-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.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 03:40:44 PM UTC 2026
% Result : Satisfiable 0.96s 1.11s
% Output : Saturation 0.96s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( c4_0
| c1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ssSkC7
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
fof(f3,negated_conjecture,
( ssSkC5
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
fof(f6,negated_conjecture,
( ssSkC0
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f7,negated_conjecture,
( c4_0
| ndr1_0
| ~ ssSkC7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
fof(f9,negated_conjecture,
( c5_0
| ndr1_0
| ~ ssSkC5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
fof(f10,negated_conjecture,
( ndr1_0
| ~ ssSkC4
| ~ ssSkC3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
fof(f11,negated_conjecture,
( c3_0
| ~ c1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f12,negated_conjecture,
( ssSkC7
| c3_1(a583) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f13,negated_conjecture,
( ssSkC7
| c5_1(a583) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
fof(f14,negated_conjecture,
! [X0] :
( ssSkP3(X0)
| ndr1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
fof(f15,negated_conjecture,
( ssSkC5
| ndr1_1(a567) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
fof(f16,negated_conjecture,
( ssSkC5
| c1_1(a567) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
fof(f17,negated_conjecture,
( ssSkC5
| c2_1(a567) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
fof(f18,negated_conjecture,
! [X0] :
( ssSkP2(X0)
| ndr1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
fof(f19,negated_conjecture,
! [X0] :
( ssSkP1(X0)
| ndr1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
fof(f20,negated_conjecture,
( ssSkC1
| c5_1(a556) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
fof(f21,negated_conjecture,
! [X0] :
( ssSkP0(X0)
| ndr1_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f22,negated_conjecture,
( ssSkC0
| ndr1_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
fof(f23,negated_conjecture,
( ssSkC0
| c2_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
fof(f24,negated_conjecture,
( c3_0
| ndr1_0
| ~ c4_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f25,negated_conjecture,
( c1_0
| c1_1(a577)
| ~ ssSkC6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
fof(f26,negated_conjecture,
( c1_0
| c4_1(a577)
| ~ ssSkC6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
fof(f27,negated_conjecture,
( ~ c2_0
| ~ c4_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
fof(f28,negated_conjecture,
( c4_0
| c5_0
| ~ c3_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
fof(f29,negated_conjecture,
( c1_0
| c3_0
| ~ c2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
fof(f30,negated_conjecture,
( ssSkC7
| ~ c4_1(a583) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
fof(f31,negated_conjecture,
! [X0] :
( ssSkP3(X0)
| c3_2(X0,a579) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
fof(f32,negated_conjecture,
( ssSkC5
| c4_2(a567,a568) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
! [X0] :
( ssSkP2(X0)
| c2_2(X0,a562) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f34,negated_conjecture,
! [X0] :
( ssSkP2(X0)
| c5_2(X0,a562) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( ssSkC3
| ~ c1_1(a561) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
! [X0] :
( ssSkP1(X0)
| c1_2(X0,a557) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( ssSkC1
| ~ c4_1(a556) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
! [X0] :
( ssSkP0(X0)
| c5_2(X0,a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
! [X0] :
( ssSkP0(X0)
| c2_2(X0,a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( ssSkC0
| c2_2(a546,a547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
fof(f41,negated_conjecture,
( ssSkC0
| c5_2(a546,a547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
fof(f43,negated_conjecture,
( c4_0
| ~ c2_1(a584)
| ~ ssSkC7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( c4_0
| ~ c5_1(a584)
| ~ ssSkC7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( c3_0
| c5_1(a578)
| ~ c4_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( c5_0
| ~ c1_1(a569)
| ~ ssSkC5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( c5_0
| ~ c2_1(a569)
| ~ ssSkC5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ndr1_0
| ~ c3_0
| ~ c5_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ c3_1(a564)
| ~ ssSkC4
| ~ ssSkC3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ c1_1(a564)
| ~ ssSkC4
| ~ ssSkC3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
! [X0] :
( c2_0
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
! [X0] :
( ssSkP3(X0)
| ~ c2_2(X0,a579) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ssSkC5
| ~ c1_2(a567,a568) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
! [X0] :
( ssSkP2(X0)
| ~ c4_2(X0,a562) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
! [X0] :
( ssSkP1(X0)
| ~ c3_2(X0,a557) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
! [X0] :
( ssSkP0(X0)
| ~ c1_2(X0,a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ssSkC0
| ~ c4_2(a546,a547) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( c2_1(a585)
| ~ c1_0
| ~ c4_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( c5_1(a585)
| ~ c1_0
| ~ c4_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
fof(f61,negated_conjecture,
( c3_0
| ~ c4_0
| ~ c5_1(a550) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ c1_0
| ~ c4_0
| ~ c1_1(a585) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ c3_0
| ~ c5_0
| ~ c1_1(a565) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
! [X0] :
( ssSkC4
| c3_1(X0)
| ndr1_1(X0)
| ~ ndr1_0
| ~ ssSkP2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
! [X0] :
( c5_0
| c2_1(X0)
| ndr1_1(X0)
| ~ ndr1_0
| ~ ssSkC1
| ~ ssSkP1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
! [X0] :
( ssSkC6
| c3_1(X0)
| ndr1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
! [X0] :
( ssSkC4
| c3_1(X0)
| c1_2(X0,a563)
| ~ ndr1_0
| ~ ssSkP2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
! [X0] :
( ssSkC4
| c3_1(X0)
| c4_2(X0,a563)
| ~ ndr1_0
| ~ ssSkP2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
! [X0] :
( c5_0
| c2_1(X0)
| c2_2(X0,a558)
| ~ ndr1_0
| ~ ssSkC1
| ~ ssSkP1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
! [X0] :
( c1_0
| c5_0
| c5_1(X0)
| ndr1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
! [X0] :
( c3_0
| c3_1(X0)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
! [X0] :
( ssSkC6
| c3_1(X0)
| c2_2(X0,a576)
| ~ ndr1_0
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
! [X0] :
( ssSkC4
| c3_1(X0)
| ~ ndr1_0
| ~ c2_2(X0,a563)
| ~ ssSkP2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
! [X0] :
( c2_0
| ndr1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ ssSkC2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
! [X0] :
( c5_0
| c2_1(X0)
| ~ ndr1_0
| ~ c5_2(X0,a558)
| ~ ssSkC1
| ~ ssSkP1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
! [X0] :
( c5_0
| c2_1(X0)
| ~ ndr1_0
| ~ c3_2(X0,a558)
| ~ ssSkC1
| ~ ssSkP1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
! [X0] :
( c1_0
| c1_1(X0)
| c4_1(X0)
| ~ c3_0
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
! [X0] :
( c5_0
| c3_2(a569,X0)
| ~ ndr1_1(a569)
| ~ c2_2(a569,X0)
| ~ ssSkC5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
! [X0] :
( ssSkC6
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c5_2(X0,a576) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
! [X0,X1] :
( c2_1(X1)
| ndr1_1(X1)
| c4_1(X0)
| ~ c4_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
! [X0] :
( c2_0
| c5_2(X0,a560)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ ssSkC2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
! [X0] :
( c2_0
| c3_2(X0,a560)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ ssSkC2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
! [X0] :
( c1_0
| c5_0
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c5_2(X0,a555) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
! [X0] :
( c1_0
| c5_0
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_2(X0,a555) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
! [X0] :
( c1_0
| c5_0
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c4_2(X0,a555) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
! [X0] :
( c3_0
| c4_2(a578,X0)
| ~ c4_0
| ~ ndr1_1(a578)
| ~ c5_2(a578,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
! [X0] :
( ~ c4_0
| ~ c1_1(a551)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
! [X0,X1] :
( c2_1(X1)
| c2_2(X1,a575)
| c4_1(X0)
| ~ c4_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
! [X0,X1] :
( c2_1(X1)
| c1_2(X1,a575)
| c4_1(X0)
| ~ c4_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
! [X0] :
( ndr1_1(a571)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
! [X0] :
( c1_1(a571)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
! [X0,X1] :
( c2_1(X1)
| c4_1(X0)
| ~ c4_1(X1)
| ~ c3_2(X1,a575)
| ~ ndr1_0
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
! [X0] :
( c3_2(a571,a573)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
! [X0] :
( c1_2(a571,a573)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
! [X0] :
( c5_2(a571,a572)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
! [X0] :
( ~ c3_0
| ~ c5_0
| ~ ndr1_1(a565)
| ~ c2_2(a565,X0)
| ~ c1_2(a565,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
! [X0] :
( c1_1(X0)
| ~ c2_0
| ~ c4_2(a571,a573)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
! [X0] :
( c1_1(X0)
| ~ c2_0
| ~ c3_2(a571,a572)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
! [X0] :
( c1_1(X0)
| ~ c2_0
| ~ c1_2(a571,a572)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
! [X0] :
( ssSkC3
| ~ ndr1_1(a561)
| ~ c2_2(a561,X0)
| ~ c4_2(a561,X0)
| ~ c5_2(a561,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
! [X0,X1] :
( ndr1_1(a552)
| c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
! [X0,X1] :
( c5_0
| c2_1(X0)
| c1_2(X0,X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
! [X0,X1] :
( c5_1(X0)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
! [X0,X1] :
( c5_0
| c2_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ c5_1(X0)
| ~ c2_2(X0,a570)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f106,negated_conjecture,
! [X0,X1] :
( c5_0
| c2_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ c5_1(X0)
| ~ c4_2(X0,a570)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
! [X0,X1] :
( c2_2(a552,a553)
| c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
! [X0,X1] :
( c1_2(a552,a553)
| c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
! [X0,X1] :
( c1_0
| c3_1(X0)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
! [X2,X0,X1] :
( c5_1(X1)
| ndr1_1(X0)
| c5_2(X1,X2)
| ~ ndr1_0
| ~ c1_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c4_1(X1)
| ~ c3_1(X0)
| ~ ssSkP3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
! [X0,X1] :
( ndr1_1(a581)
| c5_1(X0)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
! [X0,X1] :
( c3_1(a581)
| c5_1(X0)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
! [X0,X1] :
( c5_0
| c5_1(a574)
| c2_1(X0)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
! [X0,X1] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(a552,a554)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
! [X0,X1] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c4_2(a552,a554)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
! [X0,X1] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(a552,a553)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
! [X2,X0,X1] :
( c5_1(X1)
| c2_2(X0,a580)
| c5_2(X1,X2)
| ~ ndr1_0
| ~ c1_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c4_1(X1)
| ~ c3_1(X0)
| ~ ssSkP3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
! [X0,X1] :
( c5_2(a581,a582)
| c5_1(X0)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
! [X0,X1] :
( c1_2(a581,a582)
| c5_1(X0)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
! [X0,X1] :
( c5_1(X0)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c2_1(a581)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
! [X0,X1] :
( c5_0
| c2_1(X0)
| c2_2(X0,X1)
| ~ c1_1(a574)
| ~ ndr1_0
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
! [X0,X1] :
( c4_2(a551,X1)
| c5_2(a551,X1)
| ~ c4_0
| ~ ndr1_1(a551)
| ~ c2_2(a551,X1)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
! [X2,X0,X1] :
( ssSkC2
| c3_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
! [X2,X0,X1] :
( ssSkC2
| c4_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
! [X2,X0,X1] :
( c5_2(X0,a586)
| c3_2(X0,X1)
| c5_1(X2)
| c1_1(X2)
| c4_1(X2)
| ~ c3_0
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
! [X2,X0,X1] :
( c5_2(X1,X2)
| c5_1(X1)
| ~ c1_2(X1,X2)
| ~ ndr1_0
| ~ ndr1_1(X1)
| ~ c4_1(X1)
| ~ c1_2(X0,a580)
| ~ c3_1(X0)
| ~ ssSkP3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
! [X0,X1] :
( c5_1(X0)
| c4_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c2_2(a581,a582)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
! [X0,X1] :
( c1_2(a551,X1)
| ~ c4_0
| ~ ndr1_1(a551)
| ~ c3_2(a551,X1)
| ~ c4_2(a551,X1)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
! [X2,X0,X1] :
( ssSkC2
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ c1_2(X0,a559)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
! [X2,X0,X1] :
( c3_2(X0,X1)
| c5_1(X2)
| c1_1(X2)
| c4_1(X2)
| ~ c3_0
| ~ c5_1(X0)
| ~ c4_2(X0,a586)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
! [X2,X0,X1] :
( c3_2(X0,X1)
| c5_1(X2)
| c1_1(X2)
| c4_1(X2)
| ~ c3_0
| ~ c5_1(X0)
| ~ c1_2(X0,a586)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
! [X2,X0,X1] :
( c4_2(X1,a566)
| c3_2(X1,X2)
| ~ c1_1(X1)
| ~ ndr1_1(X1)
| ~ c2_2(X1,X2)
| ~ c4_2(X1,X2)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c5_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
! [X2,X0,X1] :
( c3_2(X1,X2)
| ~ c1_1(X1)
| ~ c2_2(X1,a566)
| ~ ndr1_1(X1)
| ~ c2_2(X1,X2)
| ~ c4_2(X1,X2)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c5_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f134,negated_conjecture,
! [X2,X0,X1] :
( c3_2(X1,X2)
| ~ c1_1(X1)
| ~ c3_2(X1,a566)
| ~ ndr1_1(X1)
| ~ c2_2(X1,X2)
| ~ c4_2(X1,X2)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c5_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause134) ).
fof(f135,negated_conjecture,
! [X2,X3,X0,X1] :
( c5_2(X0,a549)
| c1_2(X0,X3)
| c2_1(X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ ndr1_1(X1)
| ~ c3_2(X1,X2)
| ~ c2_2(X1,X2)
| ~ ssSkC0
| ~ ssSkP0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
! [X2,X3,X0,X1] :
( c2_2(X0,a549)
| c1_2(X0,X3)
| c2_1(X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ ndr1_1(X1)
| ~ c3_2(X1,X2)
| ~ c2_2(X1,X2)
| ~ ssSkC0
| ~ ssSkP0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
! [X2,X3,X0,X1] :
( c1_2(X0,X3)
| c2_1(X1)
| ~ c4_2(X0,a549)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ ndr1_1(X1)
| ~ c3_2(X1,X2)
| ~ c2_2(X1,X2)
| ~ ssSkC0
| ~ ssSkP0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
! [X2,X0,X1] :
( c5_0
| c3_2(a574,X2)
| c4_2(a574,X2)
| c2_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(a574)
| ~ c1_2(a574,X2)
| ~ ndr1_0
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
tcf(c_187,negated_conjecture,
( c4_0
| c1_0 ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_188,negated_conjecture,
( ssSkC7
| ndr1_0 ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_189,negated_conjecture,
( ssSkC5
| ndr1_0 ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_192,negated_conjecture,
( ssSkC0
| ndr1_0 ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_193,negated_conjecture,
( ndr1_0
| c4_0
| ~ ssSkC7 ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_195,negated_conjecture,
( c5_0
| ndr1_0
| ~ ssSkC5 ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_196,negated_conjecture,
( ndr1_0
| ~ ssSkC4
| ~ ssSkC3 ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_197,negated_conjecture,
( c3_0
| ~ c1_0 ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_198,negated_conjecture,
( ssSkC7
| c3_1(a583) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_199,negated_conjecture,
( ssSkC7
| c5_1(a583) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_200,negated_conjecture,
! [X0: $i] :
( ssSkP3(X0)
| ndr1_1(X0) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_201,negated_conjecture,
( ssSkC5
| ndr1_1(a567) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_202,negated_conjecture,
( ssSkC5
| c1_1(a567) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_203,negated_conjecture,
( ssSkC5
| c2_1(a567) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_204,negated_conjecture,
! [X0: $i] :
( ssSkP2(X0)
| ndr1_1(X0) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_205,negated_conjecture,
! [X0: $i] :
( ssSkP1(X0)
| ndr1_1(X0) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_206,negated_conjecture,
( ssSkC1
| c5_1(a556) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_207,negated_conjecture,
! [X0: $i] :
( ssSkP0(X0)
| ndr1_1(X0) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_208,negated_conjecture,
( ssSkC0
| ndr1_1(a546) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_209,negated_conjecture,
( ssSkC0
| c2_1(a546) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_210,negated_conjecture,
( c3_0
| ndr1_0
| ~ c4_0 ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_211,negated_conjecture,
( c1_0
| c1_1(a577)
| ~ ssSkC6 ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_212,negated_conjecture,
( c1_0
| c4_1(a577)
| ~ ssSkC6 ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_213,negated_conjecture,
( ~ c2_0
| ~ c4_0 ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_214,negated_conjecture,
( c5_0
| c4_0
| ~ c3_0 ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_215,negated_conjecture,
( c3_0
| c1_0
| ~ c2_0 ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_216,negated_conjecture,
( ssSkC7
| ~ c4_1(a583) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_217,negated_conjecture,
! [X0: $i] :
( ssSkP3(X0)
| c3_2(X0,a579) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_218,negated_conjecture,
( ssSkC5
| c4_2(a567,a568) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_219,negated_conjecture,
! [X0: $i] :
( ssSkP2(X0)
| c2_2(X0,a562) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_220,negated_conjecture,
! [X0: $i] :
( ssSkP2(X0)
| c5_2(X0,a562) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_221,negated_conjecture,
( ssSkC3
| ~ c1_1(a561) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_222,negated_conjecture,
! [X0: $i] :
( ssSkP1(X0)
| c1_2(X0,a557) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_223,negated_conjecture,
( ssSkC1
| ~ c4_1(a556) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_224,negated_conjecture,
! [X0: $i] :
( ssSkP0(X0)
| c5_2(X0,a548) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_225,negated_conjecture,
! [X0: $i] :
( ssSkP0(X0)
| c2_2(X0,a548) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_226,negated_conjecture,
( ssSkC0
| c2_2(a546,a547) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_227,negated_conjecture,
( ssSkC0
| c5_2(a546,a547) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_229,negated_conjecture,
( c4_0
| ~ ssSkC7
| ~ c2_1(a584) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_230,negated_conjecture,
( c4_0
| ~ ssSkC7
| ~ c5_1(a584) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_231,negated_conjecture,
( c3_0
| c5_1(a578)
| ~ c4_0 ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_232,negated_conjecture,
( c5_0
| ~ ssSkC5
| ~ c1_1(a569) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_233,negated_conjecture,
( c5_0
| ~ ssSkC5
| ~ c2_1(a569) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_234,negated_conjecture,
( ndr1_0
| ~ c3_0
| ~ c5_0 ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_235,negated_conjecture,
( ~ ssSkC4
| ~ ssSkC3
| ~ c3_1(a564) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_236,negated_conjecture,
( ~ ssSkC4
| ~ ssSkC3
| ~ c1_1(a564) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_237,negated_conjecture,
! [X0: $i] :
( c2_0
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_238,negated_conjecture,
! [X0: $i] :
( ssSkP3(X0)
| ~ c2_2(X0,a579) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_239,negated_conjecture,
( ssSkC5
| ~ c1_2(a567,a568) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_240,negated_conjecture,
! [X0: $i] :
( ssSkP2(X0)
| ~ c4_2(X0,a562) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_241,negated_conjecture,
! [X0: $i] :
( ssSkP1(X0)
| ~ c3_2(X0,a557) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_242,negated_conjecture,
! [X0: $i] :
( ssSkP0(X0)
| ~ c1_2(X0,a548) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_243,negated_conjecture,
( ssSkC0
| ~ c4_2(a546,a547) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_244,negated_conjecture,
( c2_1(a585)
| ~ c4_0
| ~ c1_0 ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_245,negated_conjecture,
( c5_1(a585)
| ~ c4_0
| ~ c1_0 ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_247,negated_conjecture,
( c3_0
| ~ c4_0
| ~ c5_1(a550) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_248,negated_conjecture,
( ~ c4_0
| ~ c1_0
| ~ c1_1(a585) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_249,negated_conjecture,
( ~ c3_0
| ~ c5_0
| ~ c1_1(a565) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_250,negated_conjecture,
! [X0: $i] :
( ssSkC4
| ndr1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ ssSkP2(X0) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_251,negated_conjecture,
! [X0: $i] :
( c5_0
| c2_1(X0)
| ndr1_1(X0)
| ~ ssSkC1
| ~ ndr1_0
| ~ ssSkP1(X0) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_252,negated_conjecture,
! [X0: $i] :
( ssSkC6
| ndr1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_253,negated_conjecture,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| c1_2(X0,a563)
| ~ ndr1_0
| ~ ssSkP2(X0) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_254,negated_conjecture,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| c4_2(X0,a563)
| ~ ndr1_0
| ~ ssSkP2(X0) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_255,negated_conjecture,
! [X0: $i] :
( c5_0
| c2_1(X0)
| c2_2(X0,a558)
| ~ ssSkC1
| ~ ndr1_0
| ~ ssSkP1(X0) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_256,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| ndr1_1(X0)
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_257,negated_conjecture,
! [X0: $i] :
( c3_0
| c3_1(X0)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_258,negated_conjecture,
! [X0: $i] :
( ssSkC6
| c3_1(X0)
| c2_2(X0,a576)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_259,negated_conjecture,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| ~ ndr1_0
| ~ ssSkP2(X0)
| ~ c2_2(X0,a563) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_260,negated_conjecture,
! [X0: $i] :
( c2_0
| ndr1_1(X0)
| ~ ssSkC2
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_261,negated_conjecture,
! [X0: $i] :
( c5_0
| c2_1(X0)
| ~ ssSkC1
| ~ ndr1_0
| ~ ssSkP1(X0)
| ~ c5_2(X0,a558) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_262,negated_conjecture,
! [X0: $i] :
( c5_0
| c2_1(X0)
| ~ ssSkC1
| ~ ndr1_0
| ~ ssSkP1(X0)
| ~ c3_2(X0,a558) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_263,negated_conjecture,
! [X0: $i] :
( c1_0
| c4_1(X0)
| c1_1(X0)
| ~ c3_0
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_264,negated_conjecture,
! [X0: $i] :
( c5_0
| c3_2(a569,X0)
| ~ ssSkC5
| ~ ndr1_1(a569)
| ~ c2_2(a569,X0) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_265,negated_conjecture,
! [X0: $i] :
( ssSkC6
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c5_2(X0,a576) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_266,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| ndr1_1(X1)
| ~ ndr1_0
| ~ c4_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_267,negated_conjecture,
! [X0: $i] :
( c2_0
| c5_2(X0,a560)
| ~ ssSkC2
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_268,negated_conjecture,
! [X0: $i] :
( c2_0
| c3_2(X0,a560)
| ~ ssSkC2
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_269,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c5_2(X0,a555) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_270,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_2(X0,a555) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_271,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c4_2(X0,a555) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_272,negated_conjecture,
! [X0: $i] :
( c3_0
| c4_2(a578,X0)
| ~ c4_0
| ~ ndr1_1(a578)
| ~ c5_2(a578,X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_273,negated_conjecture,
! [X0: $i] :
( ~ ndr1_0
| ~ c4_0
| ~ c1_1(a551)
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_274,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| c2_2(X1,a575)
| ~ ndr1_0
| ~ c4_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_275,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| c1_2(X1,a575)
| ~ ndr1_0
| ~ c4_1(X1)
| ~ c3_1(X0) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_276,negated_conjecture,
! [X0: $i] :
( ndr1_1(a571)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_277,negated_conjecture,
! [X0: $i] :
( c1_1(a571)
| c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_278,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c3_1(X1)
| ~ c3_2(X0,a575) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_279,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| c3_2(a571,a573)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_280,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| c1_2(a571,a573)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_281,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| c5_2(a571,a572)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_282,negated_conjecture,
! [X0: $i] :
( ~ c3_0
| ~ c5_0
| ~ ndr1_1(a565)
| ~ c1_2(a565,X0)
| ~ c2_2(a565,X0) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_283,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0)
| ~ c4_2(a571,a573) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_284,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0)
| ~ c3_2(a571,a572) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_285,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| ~ c2_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ c2_1(X0)
| ~ c1_2(a571,a572) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_286,negated_conjecture,
! [X0: $i] :
( ssSkC3
| ~ ndr1_1(a561)
| ~ c5_2(a561,X0)
| ~ c2_2(a561,X0)
| ~ c4_2(a561,X0) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_287,negated_conjecture,
! [X0: $i,X1: $i] :
( ndr1_1(a552)
| c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_288,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c2_1(X0)
| c1_2(X0,X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_289,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_1(X0)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_0
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_290,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c2_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c2_2(X0,a570)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_292,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c2_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c4_2(X0,a570)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_293,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_2(a552,a553)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_294,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(a552,a553)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_295,negated_conjecture,
! [X0: $i,X1: $i] :
( c1_0
| c3_1(X0)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_296,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ndr1_1(X2)
| c5_1(X0)
| c5_2(X0,X1)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ ssSkP3(X2)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X0,X1) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_297,negated_conjecture,
! [X0: $i,X1: $i] :
( ndr1_1(a581)
| c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_298,negated_conjecture,
! [X0: $i,X1: $i] :
( c3_1(a581)
| c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_299,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c5_1(a574)
| c2_1(X0)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_300,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c2_2(a552,a554)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_301,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c4_2(a552,a554)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_302,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(a552,a553)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_303,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c5_1(X0)
| c2_2(X2,a580)
| c5_2(X0,X1)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ ssSkP3(X2)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_304,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c5_2(a581,a582)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_305,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c1_2(a581,a582)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_306,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ c2_1(a581)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_307,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c2_1(X0)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ c1_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_308,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_2(a551,X0)
| c4_2(a551,X0)
| ~ ndr1_0
| ~ c4_0
| ~ ndr1_1(a551)
| ~ c4_1(X1)
| ~ c3_1(X1)
| ~ c2_2(a551,X0) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_309,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c3_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_310,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c4_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_311,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c5_2(X0,a586)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_312,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c5_1(X0)
| c5_2(X0,X1)
| ~ ndr1_0
| ~ c4_1(X0)
| ~ ssSkP3(X2)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X2,a580)
| ~ c1_2(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_313,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c2_2(a581,a582)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_314,negated_conjecture,
! [X0: $i,X1: $i] :
( c1_2(a551,X0)
| ~ ndr1_0
| ~ c4_0
| ~ ndr1_1(a551)
| ~ c4_1(X1)
| ~ c3_1(X1)
| ~ c4_2(a551,X0)
| ~ c3_2(a551,X0) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_315,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,a559)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_316,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c4_2(X0,a586)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_317,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a586)
| ~ c5_2(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_318,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_2(X0,a566)
| c3_2(X0,X1)
| ~ ndr1_0
| ~ c2_1(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_1(X2)
| ~ c2_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_319,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_2(X0,X1)
| ~ ndr1_0
| ~ c2_1(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_1(X2)
| ~ c2_2(X0,a566)
| ~ c2_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_320,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_2(X0,X1)
| ~ ndr1_0
| ~ c2_1(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_1(X2)
| ~ c3_2(X0,a566)
| ~ c2_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_321,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c5_2(X2,a549)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ ndr1_0
| ~ ssSkP0(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X2)
| ~ ndr1_1(X0)
| ~ c5_2(X2,X3)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_322,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c2_2(X2,a549)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ ndr1_0
| ~ ssSkP0(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X2)
| ~ ndr1_1(X0)
| ~ c5_2(X2,X3)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_323,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ ndr1_0
| ~ ssSkP0(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X2)
| ~ ndr1_1(X0)
| ~ c4_2(X2,a549)
| ~ c5_2(X2,X3)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_324,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c5_0
| c2_1(X0)
| c4_2(a574,X2)
| c3_2(a574,X2)
| c2_2(X0,X1)
| ~ ndr1_0
| ~ ndr1_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(a574,X2)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_404,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_192,c_189,c_188,c_210,c_195,c_193,c_234]) ).
tcf(c_414,negated_conjecture,
( c3_0
| ~ c2_0 ),
inference(global_subsumption_just,[status(thm)],[c_215,c_187,c_197,c_213]) ).
tcf(c_416,negated_conjecture,
( c5_0
| c4_0 ),
inference(global_subsumption_just,[status(thm)],[c_214,c_187,c_197,c_214]) ).
tcf(c_428,negated_conjecture,
( c3_0
| c5_1(a578) ),
inference(global_subsumption_just,[status(thm)],[c_231,c_187,c_197,c_231]) ).
tcf(c_432,negated_conjecture,
ndr1_0,
inference(global_subsumption_just,[status(thm)],[c_196,c_189,c_188,c_210,c_195,c_193,c_234]) ).
tcf(c_434,negated_conjecture,
( c3_0
| ~ c5_1(a550) ),
inference(global_subsumption_just,[status(thm)],[c_247,c_187,c_197,c_247]) ).
tcf(c_438,negated_conjecture,
! [X0: $i] :
( c2_0
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_237,c_189,c_188,c_210,c_195,c_193,c_234,c_237]) ).
tcf(c_441,negated_conjecture,
! [X0: $i] :
( ssSkC6
| ndr1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_252,c_189,c_188,c_210,c_195,c_193,c_234,c_252]) ).
tcf(c_444,negated_conjecture,
! [X0: $i] :
( ssSkC4
| ndr1_1(X0)
| c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_250,c_189,c_188,c_210,c_204,c_195,c_193,c_234,c_250]) ).
tcf(c_447,negated_conjecture,
! [X0: $i] :
( ssSkC6
| c3_1(X0)
| c2_2(X0,a576)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_258,c_189,c_188,c_210,c_195,c_193,c_234,c_258]) ).
tcf(c_450,negated_conjecture,
! [X0: $i] :
( c3_0
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_257,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_414]) ).
tcf(c_453,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| ndr1_1(X0)
| c5_1(X0)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_256,c_189,c_188,c_210,c_195,c_193,c_234,c_256]) ).
tcf(c_456,negated_conjecture,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| c4_2(X0,a563)
| ~ ssSkP2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_254,c_189,c_188,c_210,c_195,c_193,c_234,c_254]) ).
tcf(c_459,negated_conjecture,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| c1_2(X0,a563)
| ~ ssSkP2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_253,c_189,c_188,c_210,c_195,c_193,c_234,c_253]) ).
tcf(c_462,plain,
! [X0: $i] :
( ssSkC6
| c3_1(X0)
| ~ c5_2(X0,a576)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_265,c_189,c_188,c_210,c_195,c_193,c_234,c_265]) ).
tcf(c_463,negated_conjecture,
! [X0: $i] :
( ssSkC6
| c3_1(X0)
| ~ c2_1(X0)
| ~ c5_2(X0,a576) ),
inference(renaming,[status(thm)],[c_462]) ).
tcf(c_465,negated_conjecture,
! [X0: $i] :
( c1_0
| c4_1(X0)
| c1_1(X0)
| ~ c3_0
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_263,c_189,c_188,c_210,c_195,c_193,c_234,c_263]) ).
tcf(c_468,plain,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| ~ c2_2(X0,a563)
| ~ ssSkP2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_259,c_189,c_188,c_210,c_195,c_193,c_234,c_259]) ).
tcf(c_469,negated_conjecture,
! [X0: $i] :
( ssSkC4
| c3_1(X0)
| ~ ssSkP2(X0)
| ~ c2_2(X0,a563) ),
inference(renaming,[status(thm)],[c_468]) ).
tcf(c_471,plain,
! [X0: $i] :
( c5_0
| ~ ssSkC1
| ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_251,c_189,c_188,c_213,c_210,c_205,c_195,c_193,c_234,c_237,c_251,c_416]) ).
tcf(c_472,negated_conjecture,
! [X0: $i] :
( c5_0
| ndr1_1(X0)
| ~ ssSkC1 ),
inference(renaming,[status(thm)],[c_471]) ).
tcf(c_474,plain,
! [X0: $i] :
( ~ c3_1(X0)
| ~ c4_1(X0)
| ~ c1_1(a551)
| ~ c4_0 ),
inference(global_subsumption_just,[status(thm)],[c_273,c_189,c_188,c_210,c_195,c_193,c_234,c_273]) ).
tcf(c_475,negated_conjecture,
! [X0: $i] :
( ~ c4_0
| ~ c1_1(a551)
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_474]) ).
tcf(c_477,plain,
! [X0: $i] :
( c3_0
| c4_2(a578,X0)
| ~ c5_2(a578,X0)
| ~ ndr1_1(a578) ),
inference(global_subsumption_just,[status(thm)],[c_272,c_187,c_197,c_272]) ).
tcf(c_478,negated_conjecture,
! [X0: $i] :
( c3_0
| c4_2(a578,X0)
| ~ ndr1_1(a578)
| ~ c5_2(a578,X0) ),
inference(renaming,[status(thm)],[c_477]) ).
tcf(c_480,plain,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ c4_2(X0,a555)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_271,c_189,c_188,c_210,c_195,c_193,c_234,c_271]) ).
tcf(c_481,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ c3_1(X0)
| ~ c4_2(X0,a555) ),
inference(renaming,[status(thm)],[c_480]) ).
tcf(c_483,plain,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ c1_2(X0,a555)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_270,c_189,c_188,c_210,c_195,c_193,c_234,c_270]) ).
tcf(c_484,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ c3_1(X0)
| ~ c1_2(X0,a555) ),
inference(renaming,[status(thm)],[c_483]) ).
tcf(c_486,plain,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ c5_2(X0,a555)
| ~ c3_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_269,c_189,c_188,c_210,c_195,c_193,c_234,c_269]) ).
tcf(c_487,negated_conjecture,
! [X0: $i] :
( c5_0
| c1_0
| c5_1(X0)
| ~ c3_1(X0)
| ~ c5_2(X0,a555) ),
inference(renaming,[status(thm)],[c_486]) ).
tcf(c_489,plain,
! [X0: $i] :
( c2_0
| ndr1_1(X0)
| ~ ssSkC2
| ~ c3_1(X0)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_260,c_189,c_188,c_210,c_195,c_193,c_234,c_260]) ).
tcf(c_490,negated_conjecture,
! [X0: $i] :
( c2_0
| ndr1_1(X0)
| ~ ssSkC2
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_489]) ).
tcf(c_492,plain,
! [X0: $i] :
( c5_0
| ~ ssSkP1(X0)
| ~ ssSkC1
| c2_2(X0,a558) ),
inference(global_subsumption_just,[status(thm)],[c_255,c_189,c_188,c_213,c_210,c_195,c_193,c_234,c_237,c_255,c_416]) ).
tcf(c_493,negated_conjecture,
! [X0: $i] :
( c5_0
| c2_2(X0,a558)
| ~ ssSkC1
| ~ ssSkP1(X0) ),
inference(renaming,[status(thm)],[c_492]) ).
tcf(c_495,negated_conjecture,
! [X0: $i] :
( c1_1(a571)
| c1_1(X0)
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_277,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_277]) ).
tcf(c_498,negated_conjecture,
! [X0: $i] :
( ndr1_1(a571)
| c1_1(X0)
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_276,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_276]) ).
tcf(c_501,plain,
! [X0: $i] :
( c2_0
| c3_2(X0,a560)
| ~ ssSkC2
| ~ c3_1(X0)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_268,c_189,c_188,c_210,c_195,c_193,c_234,c_268]) ).
tcf(c_502,negated_conjecture,
! [X0: $i] :
( c2_0
| c3_2(X0,a560)
| ~ ssSkC2
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_501]) ).
tcf(c_504,plain,
! [X0: $i] :
( c2_0
| c5_2(X0,a560)
| ~ ssSkC2
| ~ c3_1(X0)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_267,c_189,c_188,c_210,c_195,c_193,c_234,c_267]) ).
tcf(c_505,negated_conjecture,
! [X0: $i] :
( c2_0
| c5_2(X0,a560)
| ~ ssSkC2
| ~ c4_1(X0)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_504]) ).
tcf(c_507,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| ndr1_1(X1)
| ~ c3_1(X0)
| ~ c4_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_266,c_189,c_188,c_210,c_195,c_193,c_234,c_266]) ).
tcf(c_508,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| ndr1_1(X1)
| ~ c4_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_507]) ).
tcf(c_509,plain,
! [X0: $i] :
( c5_0
| ~ ssSkP1(X0)
| ~ c3_2(X0,a558)
| ~ ssSkC1 ),
inference(global_subsumption_just,[status(thm)],[c_262,c_189,c_188,c_213,c_210,c_195,c_193,c_234,c_237,c_262,c_416]) ).
tcf(c_510,negated_conjecture,
! [X0: $i] :
( c5_0
| ~ ssSkC1
| ~ ssSkP1(X0)
| ~ c3_2(X0,a558) ),
inference(renaming,[status(thm)],[c_509]) ).
tcf(c_512,plain,
! [X0: $i] :
( c5_0
| ~ ssSkP1(X0)
| ~ c5_2(X0,a558)
| ~ ssSkC1 ),
inference(global_subsumption_just,[status(thm)],[c_261,c_189,c_188,c_213,c_210,c_195,c_193,c_234,c_237,c_261,c_416]) ).
tcf(c_513,negated_conjecture,
! [X0: $i] :
( c5_0
| ~ ssSkC1
| ~ ssSkP1(X0)
| ~ c5_2(X0,a558) ),
inference(renaming,[status(thm)],[c_512]) ).
tcf(c_515,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| c5_2(a571,a572)
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_281,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_281]) ).
tcf(c_518,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| c1_2(a571,a573)
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_280,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_280]) ).
tcf(c_521,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| c3_2(a571,a573)
| ~ c4_1(X0)
| ~ c2_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_279,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_279]) ).
tcf(c_524,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| c1_2(X1,a575)
| ~ c3_1(X0)
| ~ c4_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_275,c_189,c_188,c_210,c_195,c_193,c_234,c_275]) ).
tcf(c_525,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| c1_2(X1,a575)
| ~ c4_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_524]) ).
tcf(c_526,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| c2_2(X1,a575)
| ~ c3_1(X0)
| ~ c4_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_274,c_189,c_188,c_210,c_195,c_193,c_234,c_274]) ).
tcf(c_527,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_1(X1)
| c2_2(X1,a575)
| ~ c4_1(X1)
| ~ c3_1(X0) ),
inference(renaming,[status(thm)],[c_526]) ).
tcf(c_528,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| ~ c4_1(X0)
| ~ c2_1(X0)
| ~ c1_2(a571,a572) ),
inference(global_subsumption_just,[status(thm)],[c_285,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_285]) ).
tcf(c_531,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| ~ c4_1(X0)
| ~ c2_1(X0)
| ~ c3_2(a571,a572) ),
inference(global_subsumption_just,[status(thm)],[c_284,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_284]) ).
tcf(c_534,negated_conjecture,
! [X0: $i] :
( c1_1(X0)
| ~ c4_1(X0)
| ~ c2_1(X0)
| ~ c4_2(a571,a573) ),
inference(global_subsumption_just,[status(thm)],[c_283,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_283]) ).
tcf(c_537,plain,
! [X0: $i,X1: $i] :
( c4_1(X1)
| c2_1(X0)
| ~ c3_2(X0,a575)
| ~ c3_1(X1)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_278,c_189,c_188,c_210,c_195,c_193,c_234,c_278]) ).
tcf(c_538,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X1)
| c2_1(X0)
| ~ c4_1(X0)
| ~ c3_1(X1)
| ~ c3_2(X0,a575) ),
inference(renaming,[status(thm)],[c_537]) ).
tcf(c_539,negated_conjecture,
( c5_0
| ~ c2_0 ),
inference(global_subsumption_just,[status(thm)],[c_292,c_213,c_416]) ).
tcf(c_543,negated_conjecture,
( c5_0
| ~ c2_0 ),
inference(global_subsumption_just,[status(thm)],[c_290,c_539]) ).
tcf(c_545,plain,
! [X0: $i,X1: $i] :
( c5_1(X0)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_0
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_289,c_189,c_188,c_210,c_195,c_193,c_234,c_289]) ).
tcf(c_546,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_1(X0)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_0
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ),
inference(renaming,[status(thm)],[c_545]) ).
tcf(c_548,plain,
! [X0: $i,X1: $i] :
( c5_0
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1)
| c1_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_288,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_288,c_539]) ).
tcf(c_549,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c1_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(renaming,[status(thm)],[c_548]) ).
tcf(c_551,plain,
! [X0: $i,X1: $i] :
( ndr1_1(a552)
| c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_287,c_189,c_188,c_210,c_195,c_193,c_234,c_287]) ).
tcf(c_552,negated_conjecture,
! [X0: $i,X1: $i] :
( ndr1_1(a552)
| c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_551]) ).
tcf(c_554,plain,
! [X0: $i,X1: $i] :
( c5_2(a551,X0)
| c4_2(a551,X0)
| ~ c2_2(a551,X0)
| ~ c3_1(X1)
| ~ c4_1(X1)
| ~ ndr1_1(a551)
| ~ c4_0 ),
inference(global_subsumption_just,[status(thm)],[c_308,c_189,c_188,c_210,c_195,c_193,c_234,c_308]) ).
tcf(c_555,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_2(a551,X0)
| c4_2(a551,X0)
| ~ c4_0
| ~ ndr1_1(a551)
| ~ c4_1(X1)
| ~ c3_1(X1)
| ~ c2_2(a551,X0) ),
inference(renaming,[status(thm)],[c_554]) ).
tcf(c_557,negated_conjecture,
( c1_0
| ~ c2_0 ),
inference(global_subsumption_just,[status(thm)],[c_295,c_187,c_213]) ).
tcf(c_559,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(a552,a553)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_294,c_189,c_188,c_210,c_195,c_193,c_234,c_294]) ).
tcf(c_560,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(a552,a553)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_559]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_2(a552,a553)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_293,c_189,c_188,c_210,c_195,c_193,c_234,c_293]) ).
tcf(c_563,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c2_2(a552,a553)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_562]) ).
tcf(c_565,plain,
! [X0: $i,X1: $i] :
( c1_2(a551,X0)
| ~ c3_2(a551,X0)
| ~ c4_2(a551,X0)
| ~ c3_1(X1)
| ~ c4_1(X1)
| ~ ndr1_1(a551)
| ~ c4_0 ),
inference(global_subsumption_just,[status(thm)],[c_314,c_189,c_188,c_210,c_195,c_193,c_234,c_314]) ).
tcf(c_566,negated_conjecture,
! [X0: $i,X1: $i] :
( c1_2(a551,X0)
| ~ c4_0
| ~ ndr1_1(a551)
| ~ c4_1(X1)
| ~ c3_1(X1)
| ~ c4_2(a551,X0)
| ~ c3_2(a551,X0) ),
inference(renaming,[status(thm)],[c_565]) ).
tcf(c_568,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c3_2(a552,a553)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_302,c_189,c_188,c_210,c_195,c_193,c_234,c_302]) ).
tcf(c_569,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c3_2(a552,a553)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_568]) ).
tcf(c_571,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c4_2(a552,a554)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_301,c_189,c_188,c_210,c_195,c_193,c_234,c_301]) ).
tcf(c_572,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c4_2(a552,a554)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_571]) ).
tcf(c_574,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(a552,a554)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_300,c_189,c_188,c_210,c_195,c_193,c_234,c_300]) ).
tcf(c_575,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_1(X0)
| ~ c2_2(a552,a554)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_574]) ).
tcf(c_577,plain,
! [X0: $i,X1: $i] :
( c5_0
| c5_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_299,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_299,c_539]) ).
tcf(c_578,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c5_1(a574)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_577]) ).
tcf(c_580,plain,
! [X0: $i,X1: $i] :
( c3_1(a581)
| c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_298,c_189,c_188,c_210,c_195,c_193,c_234,c_298]) ).
tcf(c_581,negated_conjecture,
! [X0: $i,X1: $i] :
( c3_1(a581)
| c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_580]) ).
tcf(c_583,plain,
! [X0: $i,X1: $i] :
( ndr1_1(a581)
| c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_297,c_189,c_188,c_210,c_195,c_193,c_234,c_297]) ).
tcf(c_584,negated_conjecture,
! [X0: $i,X1: $i] :
( ndr1_1(a581)
| c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_583]) ).
tcf(c_586,plain,
! [X0: $i,X1: $i] :
( c5_0
| ~ c1_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_307,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_307,c_539]) ).
tcf(c_587,negated_conjecture,
! [X0: $i,X1: $i] :
( c5_0
| c2_2(X0,X1)
| ~ c1_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_586]) ).
tcf(c_589,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_1(a581) ),
inference(global_subsumption_just,[status(thm)],[c_306,c_306,c_404]) ).
tcf(c_590,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c2_1(a581)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_589]) ).
tcf(c_592,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c1_2(a581,a582)
| c4_2(X0,X1)
| ~ c2_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_305,c_189,c_188,c_210,c_195,c_193,c_234,c_305]) ).
tcf(c_593,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c1_2(a581,a582)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_592]) ).
tcf(c_595,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c5_2(a581,a582)
| c4_2(X0,X1)
| ~ c2_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_304,c_189,c_188,c_210,c_195,c_193,c_234,c_304]) ).
tcf(c_596,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c5_2(a581,a582)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_595]) ).
tcf(c_598,plain,
! [X0: $i,X1: $i,X2: $i] :
( ndr1_1(X2)
| c5_1(X0)
| c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_1(X2)
| ~ ndr1_1(X0)
| ~ ssSkP3(X2)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_296,c_189,c_188,c_210,c_195,c_193,c_234,c_296]) ).
tcf(c_599,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ndr1_1(X2)
| c5_1(X0)
| c5_2(X0,X1)
| ~ c4_1(X0)
| ~ ssSkP3(X2)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X0,X1) ),
inference(renaming,[status(thm)],[c_598]) ).
tcf(c_600,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c2_2(a581,a582)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_313,c_189,c_188,c_210,c_195,c_193,c_234,c_313]) ).
tcf(c_601,negated_conjecture,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_0
| ~ ndr1_1(X0)
| ~ c2_2(a581,a582)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_600]) ).
tcf(c_603,plain,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c5_2(X0,a586)
| c3_2(X0,X1)
| ~ c3_0
| ~ c5_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_311,c_189,c_188,c_210,c_195,c_193,c_234,c_311]) ).
tcf(c_604,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c5_2(X0,a586)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_603]) ).
tcf(c_605,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c4_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_310,c_189,c_188,c_210,c_195,c_193,c_234,c_310]) ).
tcf(c_606,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c4_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_605]) ).
tcf(c_607,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c3_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_309,c_189,c_188,c_210,c_195,c_193,c_234,c_309]) ).
tcf(c_608,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c3_2(X0,a559)
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_607]) ).
tcf(c_609,plain,
! [X0: $i,X1: $i,X2: $i] :
( c5_1(X0)
| c2_2(X2,a580)
| c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_1(X2)
| ~ ndr1_1(X0)
| ~ ssSkP3(X2)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_303,c_189,c_188,c_210,c_195,c_193,c_234,c_303]) ).
tcf(c_610,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c5_1(X0)
| c2_2(X2,a580)
| c5_2(X0,X1)
| ~ c4_1(X0)
| ~ ssSkP3(X2)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X0,X1) ),
inference(renaming,[status(thm)],[c_609]) ).
tcf(c_612,plain,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c3_2(X0,X1)
| ~ c3_0
| ~ c5_2(X0,X1)
| ~ c1_2(X0,a586)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_317,c_189,c_188,c_210,c_195,c_193,c_234,c_317]) ).
tcf(c_613,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a586)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_612]) ).
tcf(c_614,plain,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c3_2(X0,X1)
| ~ c3_0
| ~ c5_2(X0,X1)
| ~ c4_2(X0,a586)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_316,c_189,c_188,c_210,c_195,c_193,c_234,c_316]) ).
tcf(c_615,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_1(X2)
| c1_1(X2)
| c5_1(X2)
| c3_2(X0,X1)
| ~ c3_0
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c4_2(X0,a586)
| ~ c5_2(X0,X1) ),
inference(renaming,[status(thm)],[c_614]) ).
tcf(c_616,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c1_2(X0,a559)
| ~ ndr1_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_315,c_189,c_188,c_210,c_195,c_193,c_234,c_315]) ).
tcf(c_617,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ssSkC2
| c1_2(X0,X2)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,a559)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_616]) ).
tcf(c_618,plain,
! [X0: $i,X1: $i,X2: $i] :
( c5_1(X0)
| c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c1_2(X2,a580)
| ~ c3_1(X2)
| ~ ndr1_1(X0)
| ~ ssSkP3(X2)
| ~ c4_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_312,c_189,c_188,c_210,c_195,c_193,c_234,c_312]) ).
tcf(c_619,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c5_1(X0)
| c5_2(X0,X1)
| ~ c4_1(X0)
| ~ ssSkP3(X2)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X2,a580)
| ~ c1_2(X0,X1) ),
inference(renaming,[status(thm)],[c_618]) ).
tcf(c_621,plain,
! [X0: $i,X1: $i,X2: $i] :
( c4_2(X0,a566)
| c3_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_1(X2)
| ~ ndr1_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_318,c_189,c_188,c_210,c_195,c_193,c_234,c_318]) ).
tcf(c_622,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c4_2(X0,a566)
| c3_2(X0,X1)
| ~ c2_1(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_1(X2)
| ~ c2_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(renaming,[status(thm)],[c_621]) ).
tcf(c_624,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,a566)
| ~ c5_1(X2)
| ~ ndr1_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_320,c_189,c_188,c_210,c_195,c_193,c_234,c_320]) ).
tcf(c_625,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_2(X0,X1)
| ~ c2_1(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_1(X2)
| ~ c3_2(X0,a566)
| ~ c2_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(renaming,[status(thm)],[c_624]) ).
tcf(c_627,plain,
! [X0: $i,X1: $i,X2: $i] :
( c3_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a566)
| ~ c5_1(X2)
| ~ ndr1_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_319,c_189,c_188,c_210,c_195,c_193,c_234,c_319]) ).
tcf(c_628,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c3_2(X0,X1)
| ~ c2_1(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_1(X2)
| ~ c2_2(X0,a566)
| ~ c2_2(X0,X1)
| ~ c4_2(X0,X1) ),
inference(renaming,[status(thm)],[c_627]) ).
tcf(c_630,plain,
! [X0: $i,X1: $i,X2: $i] :
( c5_0
| ~ ndr1_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(a574,X2)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1)
| c2_2(X0,X1)
| c3_2(a574,X2)
| c4_2(a574,X2) ),
inference(global_subsumption_just,[status(thm)],[c_324,c_189,c_188,c_210,c_195,c_193,c_234,c_237,c_324,c_539]) ).
tcf(c_631,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( c5_0
| c4_2(a574,X2)
| c3_2(a574,X2)
| c2_2(X0,X1)
| ~ ndr1_1(a574)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(a574,X2)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_630]) ).
tcf(c_633,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c2_2(X2,a549)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X2,X3)
| ~ ndr1_1(X0)
| ~ ndr1_1(X2)
| ~ c1_1(X0)
| ~ ssSkP0(X2) ),
inference(global_subsumption_just,[status(thm)],[c_322,c_189,c_188,c_210,c_195,c_193,c_234,c_322]) ).
tcf(c_634,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c2_2(X2,a549)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ ssSkP0(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X2)
| ~ ndr1_1(X0)
| ~ c5_2(X2,X3)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_633]) ).
tcf(c_636,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c5_2(X2,a549)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X2,X3)
| ~ ndr1_1(X0)
| ~ ndr1_1(X2)
| ~ c1_1(X0)
| ~ ssSkP0(X2) ),
inference(global_subsumption_just,[status(thm)],[c_321,c_189,c_188,c_210,c_195,c_193,c_234,c_321]) ).
tcf(c_637,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c5_2(X2,a549)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ ssSkP0(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X2)
| ~ ndr1_1(X0)
| ~ c5_2(X2,X3)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_636]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X2,X3)
| ~ c4_2(X2,a549)
| ~ ndr1_1(X0)
| ~ ndr1_1(X2)
| ~ c1_1(X0)
| ~ ssSkP0(X2) ),
inference(global_subsumption_just,[status(thm)],[c_323,c_189,c_188,c_210,c_195,c_193,c_234,c_323]) ).
tcf(c_640,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c2_1(X0)
| c1_2(X2,X3)
| ~ ssSkC0
| ~ ssSkP0(X2)
| ~ c1_1(X0)
| ~ ndr1_1(X2)
| ~ ndr1_1(X0)
| ~ c4_2(X2,a549)
| ~ c5_2(X2,X3)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ),
inference(renaming,[status(thm)],[c_639]) ).
tcf(c_708,plain,
! [X0: $i,X1: $i,X2: $i] :
( ndr1_1(X2)
| c5_1(X0)
| c5_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c3_1(X2)
| ~ c1_2(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_599,c_200]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i] :
( c4_1(X0)
| c5_1(X0)
| c4_2(X0,X1)
| ~ c2_1(a581)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_590,c_438]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN538-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.36 % Computer : n013.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Fri Sep 25 01:42:21 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/0.41 Running EPR theorem proving
% 0.15/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42
% 0.15/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.42
% 0.15/0.42 % Detected problem language: tptp
% 0.15/0.43 % Proving...
% 0.96/1.11 % SZS status Started for theBenchmark.p
% 0.96/1.11 % SZS status Satisfiable for theBenchmark.p
% 0.96/1.11
% 0.96/1.11 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.96/1.11
% 0.96/1.11 % ------ iProver source info
% 0.96/1.11
% 0.96/1.11 % git: date: 2026-07-19 20:42:38 +0200
% 0.96/1.11 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.96/1.11 % git: non_committed_changes: false
% 0.96/1.11
% 0.96/1.11 % ------ Parsing...% successful
% 0.96/1.11
% 0.96/1.11
% 0.96/1.11 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 0.96/1.11 %
% 0.96/1.11
% 0.96/1.11 % ------ Preprocessing... sf_s rm: 124 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 0.96/1.11
% 0.96/1.11 % ------ Preprocessing...% ------ preprocesses with Option_epr_horn
% 0.96/1.11 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 0.96/1.11 % ------ Proving...
% 0.96/1.11 % ------ Problem Properties
% 0.96/1.11
% 0.96/1.11 %
% 0.96/1.11 % clauses 0
% 0.96/1.11 % conjectures 0
% 0.96/1.11 % EPR 0
% 0.96/1.11 % Horn 0
% 0.96/1.11 % unary 0
% 0.96/1.11 % binary 0
% 0.96/1.11 % lits 0
% 0.96/1.11 % lits eq 0
% 0.96/1.11 % fd_pure 0
% 0.96/1.11 % fd_pseudo 0
% 0.96/1.11 % fd_cond 0
% 0.96/1.11 % fd_pseudo_cond 0
% 0.96/1.11 % AC symbols 0
% 0.96/1.11
% 0.96/1.11 % ------ Schedule EPR Horn non eq is on
% 0.96/1.11
% 0.96/1.11 % ------ no conjectures: strip conj schedule
% 0.96/1.11
% 0.96/1.11 % ------ no equalities: superposition off
% 0.96/1.11
% 0.96/1.11 % ------ Option_epr_horn stripped conjectures Time Limit: Unbounded
% 0.96/1.11
% 0.96/1.11
% 0.96/1.11 %
% 0.96/1.11
% 0.96/1.11 % SZS status Satisfiable for theBenchmark.p
% 0.96/1.11
% 0.96/1.11 % SZS output start Saturation for theBenchmark.p
% See solution above
% 0.96/1.12
% 0.96/1.12
%------------------------------------------------------------------------------