%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS009-1 : TPTP v8.1.2. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:28:27 EDT 2024
% Result : Satisfiable 11.72s 11.89s
% Output : Saturation 11.72s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_31,axiom,
( t(X29,u8r2(X29))
| ~ t3least(X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_31) ).
cnf(clause_18,axiom,
( t(X18,X19)
| ~ r(X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18) ).
cnf(clause_36,axiom,
( r1most(X34)
| r(X34,u9r1(X34)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_36) ).
cnf(c15,plain,
( r1most(X61)
| t(X61,u9r1(X61)) ),
inference(resolution,[status(thm)],[clause_36,clause_18]) ).
cnf(clause_20,axiom,
( t(X20,X21)
| ~ s(X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
cnf(clause_41,axiom,
( s1most(X53)
| s(X53,u10r2(X53)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_41) ).
cnf(c40,plain,
( s1most(X65)
| t(X65,u10r2(X65)) ),
inference(resolution,[status(thm)],[clause_41,clause_20]) ).
cnf(clause_37,axiom,
( r1most(X40)
| r(X40,u9r2(X40)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_37) ).
cnf(c23,plain,
( r1most(X62)
| t(X62,u9r2(X62)) ),
inference(resolution,[status(thm)],[clause_37,clause_18]) ).
cnf(clause_33,axiom,
( t3least(X78)
| equalish(X76,X77)
| equalish(X76,X79)
| equalish(X77,X79)
| ~ t(X78,X76)
| ~ t(X78,X77)
| ~ t(X78,X79) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_33) ).
cnf(c93,plain,
( t3least(X290)
| equalish(X288,X289)
| equalish(X288,u9r2(X290))
| equalish(X289,u9r2(X290))
| ~ t(X290,X288)
| ~ t(X290,X289)
| r1most(X290) ),
inference(resolution,[status(thm)],[clause_33,c23]) ).
cnf(c700,plain,
( t3least(X932)
| equalish(X931,u10r2(X932))
| equalish(X931,u9r2(X932))
| equalish(u10r2(X932),u9r2(X932))
| ~ t(X932,X931)
| r1most(X932)
| s1most(X932) ),
inference(resolution,[status(thm)],[c93,c40]) ).
cnf(c1525,plain,
( t3least(X1922)
| equalish(u9r1(X1922),u10r2(X1922))
| equalish(u9r1(X1922),u9r2(X1922))
| equalish(u10r2(X1922),u9r2(X1922))
| r1most(X1922)
| s1most(X1922) ),
inference(resolution,[status(thm)],[c700,c15]) ).
cnf(c5531,plain,
( equalish(u9r1(X2927),u10r2(X2927))
| equalish(u9r1(X2927),u9r2(X2927))
| equalish(u10r2(X2927),u9r2(X2927))
| r1most(X2927)
| s1most(X2927)
| t(X2927,u8r2(X2927)) ),
inference(resolution,[status(thm)],[c1525,clause_31]) ).
cnf(clause_32,axiom,
( t(X30,u8r3(X30))
| ~ t3least(X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_32) ).
cnf(c5481,plain,
( equalish(u9r1(X2926),u10r2(X2926))
| equalish(u9r1(X2926),u9r2(X2926))
| equalish(u10r2(X2926),u9r2(X2926))
| r1most(X2926)
| s1most(X2926)
| t(X2926,u8r3(X2926)) ),
inference(resolution,[status(thm)],[c1525,clause_32]) ).
cnf(clause_30,axiom,
( t(X28,u8r1(X28))
| ~ t3least(X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
cnf(c5426,plain,
( equalish(u9r1(X2924),u10r2(X2924))
| equalish(u9r1(X2924),u9r2(X2924))
| equalish(u10r2(X2924),u9r2(X2924))
| r1most(X2924)
| s1most(X2924)
| t(X2924,u8r1(X2924)) ),
inference(resolution,[status(thm)],[c1525,clause_30]) ).
cnf(clause_40,axiom,
( s1most(X47)
| s(X47,u10r1(X47)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_40) ).
cnf(c34,plain,
( s1most(X64)
| t(X64,u10r1(X64)) ),
inference(resolution,[status(thm)],[clause_40,clause_20]) ).
cnf(c699,plain,
( t3least(X925)
| equalish(X924,u10r1(X925))
| equalish(X924,u9r2(X925))
| equalish(u10r1(X925),u9r2(X925))
| ~ t(X925,X924)
| r1most(X925)
| s1most(X925) ),
inference(resolution,[status(thm)],[c93,c34]) ).
cnf(c1506,plain,
( t3least(X1919)
| equalish(u9r1(X1919),u10r1(X1919))
| equalish(u9r1(X1919),u9r2(X1919))
| equalish(u10r1(X1919),u9r2(X1919))
| r1most(X1919)
| s1most(X1919) ),
inference(resolution,[status(thm)],[c699,c15]) ).
cnf(c5391,plain,
( equalish(u9r1(X2923),u10r1(X2923))
| equalish(u9r1(X2923),u9r2(X2923))
| equalish(u10r1(X2923),u9r2(X2923))
| r1most(X2923)
| s1most(X2923)
| t(X2923,u8r2(X2923)) ),
inference(resolution,[status(thm)],[c1506,clause_31]) ).
cnf(c5341,plain,
( equalish(u9r1(X2922),u10r1(X2922))
| equalish(u9r1(X2922),u9r2(X2922))
| equalish(u10r1(X2922),u9r2(X2922))
| r1most(X2922)
| s1most(X2922)
| t(X2922,u8r3(X2922)) ),
inference(resolution,[status(thm)],[c1506,clause_32]) ).
cnf(c5286,plain,
( equalish(u9r1(X2921),u10r1(X2921))
| equalish(u9r1(X2921),u9r2(X2921))
| equalish(u10r1(X2921),u9r2(X2921))
| r1most(X2921)
| s1most(X2921)
| t(X2921,u8r1(X2921)) ),
inference(resolution,[status(thm)],[c1506,clause_30]) ).
cnf(c91,plain,
( t3least(X274)
| equalish(X273,X275)
| equalish(X273,u10r2(X274))
| equalish(X275,u10r2(X274))
| ~ t(X274,X273)
| ~ t(X274,X275)
| s1most(X274) ),
inference(resolution,[status(thm)],[clause_33,c40]) ).
cnf(c645,plain,
( t3least(X906)
| equalish(X905,u9r1(X906))
| equalish(X905,u10r2(X906))
| equalish(u9r1(X906),u10r2(X906))
| ~ t(X906,X905)
| s1most(X906)
| r1most(X906) ),
inference(resolution,[status(thm)],[c91,c15]) ).
cnf(c1477,plain,
( t3least(X1901)
| equalish(u10r1(X1901),u9r1(X1901))
| equalish(u10r1(X1901),u10r2(X1901))
| equalish(u9r1(X1901),u10r2(X1901))
| s1most(X1901)
| r1most(X1901) ),
inference(resolution,[status(thm)],[c645,c34]) ).
cnf(c4527,plain,
( equalish(u10r1(X2810),u9r1(X2810))
| equalish(u10r1(X2810),u10r2(X2810))
| equalish(u9r1(X2810),u10r2(X2810))
| s1most(X2810)
| r1most(X2810)
| t(X2810,u8r2(X2810)) ),
inference(resolution,[status(thm)],[c1477,clause_31]) ).
cnf(c4477,plain,
( equalish(u10r1(X2809),u9r1(X2809))
| equalish(u10r1(X2809),u10r2(X2809))
| equalish(u9r1(X2809),u10r2(X2809))
| s1most(X2809)
| r1most(X2809)
| t(X2809,u8r3(X2809)) ),
inference(resolution,[status(thm)],[c1477,clause_32]) ).
cnf(c4422,plain,
( equalish(u10r1(X2807),u9r1(X2807))
| equalish(u10r1(X2807),u10r2(X2807))
| equalish(u9r1(X2807),u10r2(X2807))
| s1most(X2807)
| r1most(X2807)
| t(X2807,u8r1(X2807)) ),
inference(resolution,[status(thm)],[c1477,clause_30]) ).
cnf(c644,plain,
( t3least(X899)
| equalish(X898,u9r2(X899))
| equalish(X898,u10r2(X899))
| equalish(u9r2(X899),u10r2(X899))
| ~ t(X899,X898)
| s1most(X899)
| r1most(X899) ),
inference(resolution,[status(thm)],[c91,c23]) ).
cnf(c1458,plain,
( t3least(X1897)
| equalish(u10r1(X1897),u9r2(X1897))
| equalish(u10r1(X1897),u10r2(X1897))
| equalish(u9r2(X1897),u10r2(X1897))
| s1most(X1897)
| r1most(X1897) ),
inference(resolution,[status(thm)],[c644,c34]) ).
cnf(c4247,plain,
( equalish(u10r1(X2803),u9r2(X2803))
| equalish(u10r1(X2803),u10r2(X2803))
| equalish(u9r2(X2803),u10r2(X2803))
| s1most(X2803)
| r1most(X2803)
| t(X2803,u8r2(X2803)) ),
inference(resolution,[status(thm)],[c1458,clause_31]) ).
cnf(c4197,plain,
( equalish(u10r1(X2801),u9r2(X2801))
| equalish(u10r1(X2801),u10r2(X2801))
| equalish(u9r2(X2801),u10r2(X2801))
| s1most(X2801)
| r1most(X2801)
| t(X2801,u8r3(X2801)) ),
inference(resolution,[status(thm)],[c1458,clause_32]) ).
cnf(c4142,plain,
( equalish(u10r1(X2800),u9r2(X2800))
| equalish(u10r1(X2800),u10r2(X2800))
| equalish(u9r2(X2800),u10r2(X2800))
| s1most(X2800)
| r1most(X2800)
| t(X2800,u8r1(X2800)) ),
inference(resolution,[status(thm)],[c1458,clause_30]) ).
cnf(clause_35,axiom,
( r1most(X72)
| ~ equalish(u9r2(X72),u9r1(X72)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_35) ).
cnf(c94,plain,
( t3least(X295)
| equalish(X293,X294)
| equalish(X293,u9r1(X295))
| equalish(X294,u9r1(X295))
| ~ t(X295,X293)
| ~ t(X295,X294)
| r1most(X295) ),
inference(resolution,[status(thm)],[clause_33,c15]) ).
cnf(c720,plain,
( t3least(X984)
| equalish(X983,u9r2(X984))
| equalish(X983,u9r1(X984))
| equalish(u9r2(X984),u9r1(X984))
| ~ t(X984,X983)
| r1most(X984) ),
inference(resolution,[status(thm)],[c94,c23]) ).
cnf(c1711,plain,
( t3least(X1989)
| equalish(u10r2(X1989),u9r2(X1989))
| equalish(u10r2(X1989),u9r1(X1989))
| equalish(u9r2(X1989),u9r1(X1989))
| r1most(X1989)
| s1most(X1989) ),
inference(resolution,[status(thm)],[c720,c40]) ).
cnf(c7412,plain,
( t3least(X1990)
| equalish(u10r2(X1990),u9r2(X1990))
| equalish(u10r2(X1990),u9r1(X1990))
| r1most(X1990)
| s1most(X1990) ),
inference(resolution,[status(thm)],[c1711,clause_35]) ).
cnf(c7540,plain,
( equalish(u10r2(X1994),u9r2(X1994))
| equalish(u10r2(X1994),u9r1(X1994))
| r1most(X1994)
| s1most(X1994)
| t(X1994,u8r2(X1994)) ),
inference(resolution,[status(thm)],[c7412,clause_31]) ).
cnf(c7490,plain,
( equalish(u10r2(X1993),u9r2(X1993))
| equalish(u10r2(X1993),u9r1(X1993))
| r1most(X1993)
| s1most(X1993)
| t(X1993,u8r3(X1993)) ),
inference(resolution,[status(thm)],[c7412,clause_32]) ).
cnf(c7435,plain,
( equalish(u10r2(X1991),u9r2(X1991))
| equalish(u10r2(X1991),u9r1(X1991))
| r1most(X1991)
| s1most(X1991)
| t(X1991,u8r1(X1991)) ),
inference(resolution,[status(thm)],[c7412,clause_30]) ).
cnf(c1707,plain,
( t3least(X1982)
| equalish(u10r1(X1982),u9r2(X1982))
| equalish(u10r1(X1982),u9r1(X1982))
| equalish(u9r2(X1982),u9r1(X1982))
| r1most(X1982)
| s1most(X1982) ),
inference(resolution,[status(thm)],[c720,c34]) ).
cnf(c7050,plain,
( t3least(X1983)
| equalish(u10r1(X1983),u9r2(X1983))
| equalish(u10r1(X1983),u9r1(X1983))
| r1most(X1983)
| s1most(X1983) ),
inference(resolution,[status(thm)],[c1707,clause_35]) ).
cnf(c7178,plain,
( equalish(u10r1(X1987),u9r2(X1987))
| equalish(u10r1(X1987),u9r1(X1987))
| r1most(X1987)
| s1most(X1987)
| t(X1987,u8r2(X1987)) ),
inference(resolution,[status(thm)],[c7050,clause_31]) ).
cnf(c7128,plain,
( equalish(u10r1(X1985),u9r2(X1985))
| equalish(u10r1(X1985),u9r1(X1985))
| r1most(X1985)
| s1most(X1985)
| t(X1985,u8r3(X1985)) ),
inference(resolution,[status(thm)],[c7050,clause_32]) ).
cnf(c7073,plain,
( equalish(u10r1(X1984),u9r2(X1984))
| equalish(u10r1(X1984),u9r1(X1984))
| r1most(X1984)
| s1most(X1984)
| t(X1984,u8r1(X1984)) ),
inference(resolution,[status(thm)],[c7050,clause_30]) ).
cnf(c718,plain,
( t3least(X971)
| equalish(X970,u10r2(X971))
| equalish(X970,u9r1(X971))
| equalish(u10r2(X971),u9r1(X971))
| ~ t(X971,X970)
| r1most(X971)
| s1most(X971) ),
inference(resolution,[status(thm)],[c94,c40]) ).
cnf(c1665,plain,
( t3least(X1970)
| equalish(u9r2(X1970),u10r2(X1970))
| equalish(u9r2(X1970),u9r1(X1970))
| equalish(u10r2(X1970),u9r1(X1970))
| r1most(X1970)
| s1most(X1970) ),
inference(resolution,[status(thm)],[c718,c23]) ).
cnf(c6688,plain,
( t3least(X1971)
| equalish(u9r2(X1971),u10r2(X1971))
| equalish(u10r2(X1971),u9r1(X1971))
| r1most(X1971)
| s1most(X1971) ),
inference(resolution,[status(thm)],[c1665,clause_35]) ).
cnf(c6816,plain,
( equalish(u9r2(X1974),u10r2(X1974))
| equalish(u10r2(X1974),u9r1(X1974))
| r1most(X1974)
| s1most(X1974)
| t(X1974,u8r2(X1974)) ),
inference(resolution,[status(thm)],[c6688,clause_31]) ).
cnf(c6766,plain,
( equalish(u9r2(X1973),u10r2(X1973))
| equalish(u10r2(X1973),u9r1(X1973))
| r1most(X1973)
| s1most(X1973)
| t(X1973,u8r3(X1973)) ),
inference(resolution,[status(thm)],[c6688,clause_32]) ).
cnf(c6711,plain,
( equalish(u9r2(X1972),u10r2(X1972))
| equalish(u10r2(X1972),u9r1(X1972))
| r1most(X1972)
| s1most(X1972)
| t(X1972,u8r1(X1972)) ),
inference(resolution,[status(thm)],[c6688,clause_30]) ).
cnf(c717,plain,
( t3least(X964)
| equalish(X963,u10r1(X964))
| equalish(X963,u9r1(X964))
| equalish(u10r1(X964),u9r1(X964))
| ~ t(X964,X963)
| r1most(X964)
| s1most(X964) ),
inference(resolution,[status(thm)],[c94,c34]) ).
cnf(c1632,plain,
( t3least(X1956)
| equalish(u9r2(X1956),u10r1(X1956))
| equalish(u9r2(X1956),u9r1(X1956))
| equalish(u10r1(X1956),u9r1(X1956))
| r1most(X1956)
| s1most(X1956) ),
inference(resolution,[status(thm)],[c717,c23]) ).
cnf(c6326,plain,
( t3least(X1957)
| equalish(u9r2(X1957),u10r1(X1957))
| equalish(u10r1(X1957),u9r1(X1957))
| r1most(X1957)
| s1most(X1957) ),
inference(resolution,[status(thm)],[c1632,clause_35]) ).
cnf(c6454,plain,
( equalish(u9r2(X1961),u10r1(X1961))
| equalish(u10r1(X1961),u9r1(X1961))
| r1most(X1961)
| s1most(X1961)
| t(X1961,u8r2(X1961)) ),
inference(resolution,[status(thm)],[c6326,clause_31]) ).
cnf(c6404,plain,
( equalish(u9r2(X1960),u10r1(X1960))
| equalish(u10r1(X1960),u9r1(X1960))
| r1most(X1960)
| s1most(X1960)
| t(X1960,u8r3(X1960)) ),
inference(resolution,[status(thm)],[c6326,clause_32]) ).
cnf(c6349,plain,
( equalish(u9r2(X1959),u10r1(X1959))
| equalish(u10r1(X1959),u9r1(X1959))
| r1most(X1959)
| s1most(X1959)
| t(X1959,u8r1(X1959)) ),
inference(resolution,[status(thm)],[c6326,clause_30]) ).
cnf(clause_39,axiom,
( s1most(X73)
| ~ equalish(u10r2(X73),u10r1(X73)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_39) ).
cnf(c1627,plain,
( t3least(X1949)
| equalish(u10r2(X1949),u10r1(X1949))
| equalish(u10r2(X1949),u9r1(X1949))
| equalish(u10r1(X1949),u9r1(X1949))
| r1most(X1949)
| s1most(X1949) ),
inference(resolution,[status(thm)],[c717,c40]) ).
cnf(c5964,plain,
( t3least(X1950)
| equalish(u10r2(X1950),u9r1(X1950))
| equalish(u10r1(X1950),u9r1(X1950))
| r1most(X1950)
| s1most(X1950) ),
inference(resolution,[status(thm)],[c1627,clause_39]) ).
cnf(c6092,plain,
( equalish(u10r2(X1954),u9r1(X1954))
| equalish(u10r1(X1954),u9r1(X1954))
| r1most(X1954)
| s1most(X1954)
| t(X1954,u8r2(X1954)) ),
inference(resolution,[status(thm)],[c5964,clause_31]) ).
cnf(c6042,plain,
( equalish(u10r2(X1953),u9r1(X1953))
| equalish(u10r1(X1953),u9r1(X1953))
| r1most(X1953)
| s1most(X1953)
| t(X1953,u8r3(X1953)) ),
inference(resolution,[status(thm)],[c5964,clause_32]) ).
cnf(c5987,plain,
( equalish(u10r2(X1951),u9r1(X1951))
| equalish(u10r1(X1951),u9r1(X1951))
| r1most(X1951)
| s1most(X1951)
| t(X1951,u8r1(X1951)) ),
inference(resolution,[status(thm)],[c5964,clause_30]) ).
cnf(c1500,plain,
( t3least(X1910)
| equalish(u10r2(X1910),u10r1(X1910))
| equalish(u10r2(X1910),u9r2(X1910))
| equalish(u10r1(X1910),u9r2(X1910))
| r1most(X1910)
| s1most(X1910) ),
inference(resolution,[status(thm)],[c699,c40]) ).
cnf(c5042,plain,
( t3least(X1912)
| equalish(u10r2(X1912),u9r2(X1912))
| equalish(u10r1(X1912),u9r2(X1912))
| r1most(X1912)
| s1most(X1912) ),
inference(resolution,[status(thm)],[c1500,clause_39]) ).
cnf(c5170,plain,
( equalish(u10r2(X1915),u9r2(X1915))
| equalish(u10r1(X1915),u9r2(X1915))
| r1most(X1915)
| s1most(X1915)
| t(X1915,u8r2(X1915)) ),
inference(resolution,[status(thm)],[c5042,clause_31]) ).
cnf(c5120,plain,
( equalish(u10r2(X1914),u9r2(X1914))
| equalish(u10r1(X1914),u9r2(X1914))
| r1most(X1914)
| s1most(X1914)
| t(X1914,u8r3(X1914)) ),
inference(resolution,[status(thm)],[c5042,clause_32]) ).
cnf(c5065,plain,
( equalish(u10r2(X1913),u9r2(X1913))
| equalish(u10r1(X1913),u9r2(X1913))
| r1most(X1913)
| s1most(X1913)
| t(X1913,u8r1(X1913)) ),
inference(resolution,[status(thm)],[c5042,clause_30]) ).
cnf(c1486,plain,
( t3least(X1903)
| equalish(u9r2(X1903),u9r1(X1903))
| equalish(u9r2(X1903),u10r2(X1903))
| equalish(u9r1(X1903),u10r2(X1903))
| s1most(X1903)
| r1most(X1903) ),
inference(resolution,[status(thm)],[c645,c23]) ).
cnf(c4680,plain,
( t3least(X1904)
| equalish(u9r2(X1904),u10r2(X1904))
| equalish(u9r1(X1904),u10r2(X1904))
| s1most(X1904)
| r1most(X1904) ),
inference(resolution,[status(thm)],[c1486,clause_35]) ).
cnf(c4808,plain,
( equalish(u9r2(X1908),u10r2(X1908))
| equalish(u9r1(X1908),u10r2(X1908))
| s1most(X1908)
| r1most(X1908)
| t(X1908,u8r2(X1908)) ),
inference(resolution,[status(thm)],[c4680,clause_31]) ).
cnf(c4758,plain,
( equalish(u9r2(X1907),u10r2(X1907))
| equalish(u9r1(X1907),u10r2(X1907))
| s1most(X1907)
| r1most(X1907)
| t(X1907,u8r3(X1907)) ),
inference(resolution,[status(thm)],[c4680,clause_32]) ).
cnf(c4703,plain,
( equalish(u9r2(X1906),u10r2(X1906))
| equalish(u9r1(X1906),u10r2(X1906))
| s1most(X1906)
| r1most(X1906)
| t(X1906,u8r1(X1906)) ),
inference(resolution,[status(thm)],[c4680,clause_30]) ).
cnf(c90,plain,
( t3least(X266)
| equalish(X264,X265)
| equalish(X264,u10r1(X266))
| equalish(X265,u10r1(X266))
| ~ t(X266,X264)
| ~ t(X266,X265)
| s1most(X266) ),
inference(resolution,[status(thm)],[clause_33,c34]) ).
cnf(c617,plain,
( t3least(X866)
| equalish(X867,u9r1(X866))
| equalish(X867,u10r1(X866))
| equalish(u9r1(X866),u10r1(X866))
| ~ t(X866,X867)
| s1most(X866)
| r1most(X866) ),
inference(resolution,[status(thm)],[c90,c15]) ).
cnf(c1401,plain,
( t3least(X1880)
| equalish(u9r2(X1880),u9r1(X1880))
| equalish(u9r2(X1880),u10r1(X1880))
| equalish(u9r1(X1880),u10r1(X1880))
| s1most(X1880)
| r1most(X1880) ),
inference(resolution,[status(thm)],[c617,c23]) ).
cnf(c3898,plain,
( t3least(X1881)
| equalish(u9r2(X1881),u10r1(X1881))
| equalish(u9r1(X1881),u10r1(X1881))
| s1most(X1881)
| r1most(X1881) ),
inference(resolution,[status(thm)],[c1401,clause_35]) ).
cnf(c4026,plain,
( equalish(u9r2(X1884),u10r1(X1884))
| equalish(u9r1(X1884),u10r1(X1884))
| s1most(X1884)
| r1most(X1884)
| t(X1884,u8r2(X1884)) ),
inference(resolution,[status(thm)],[c3898,clause_31]) ).
cnf(c3976,plain,
( equalish(u9r2(X1883),u10r1(X1883))
| equalish(u9r1(X1883),u10r1(X1883))
| s1most(X1883)
| r1most(X1883)
| t(X1883,u8r3(X1883)) ),
inference(resolution,[status(thm)],[c3898,clause_32]) ).
cnf(c3921,plain,
( equalish(u9r2(X1882),u10r1(X1882))
| equalish(u9r1(X1882),u10r1(X1882))
| s1most(X1882)
| r1most(X1882)
| t(X1882,u8r1(X1882)) ),
inference(resolution,[status(thm)],[c3898,clause_30]) ).
cnf(c1396,plain,
( t3least(X1873)
| equalish(u10r2(X1873),u9r1(X1873))
| equalish(u10r2(X1873),u10r1(X1873))
| equalish(u9r1(X1873),u10r1(X1873))
| s1most(X1873)
| r1most(X1873) ),
inference(resolution,[status(thm)],[c617,c40]) ).
cnf(c3536,plain,
( t3least(X1874)
| equalish(u10r2(X1874),u9r1(X1874))
| equalish(u9r1(X1874),u10r1(X1874))
| s1most(X1874)
| r1most(X1874) ),
inference(resolution,[status(thm)],[c1396,clause_39]) ).
cnf(c3664,plain,
( equalish(u10r2(X1878),u9r1(X1878))
| equalish(u9r1(X1878),u10r1(X1878))
| s1most(X1878)
| r1most(X1878)
| t(X1878,u8r2(X1878)) ),
inference(resolution,[status(thm)],[c3536,clause_31]) ).
cnf(c3614,plain,
( equalish(u10r2(X1876),u9r1(X1876))
| equalish(u9r1(X1876),u10r1(X1876))
| s1most(X1876)
| r1most(X1876)
| t(X1876,u8r3(X1876)) ),
inference(resolution,[status(thm)],[c3536,clause_32]) ).
cnf(c3559,plain,
( equalish(u10r2(X1875),u9r1(X1875))
| equalish(u9r1(X1875),u10r1(X1875))
| s1most(X1875)
| r1most(X1875)
| t(X1875,u8r1(X1875)) ),
inference(resolution,[status(thm)],[c3536,clause_30]) ).
cnf(c616,plain,
( t3least(X859)
| equalish(X860,u9r2(X859))
| equalish(X860,u10r1(X859))
| equalish(u9r2(X859),u10r1(X859))
| ~ t(X859,X860)
| s1most(X859)
| r1most(X859) ),
inference(resolution,[status(thm)],[c90,c23]) ).
cnf(c1377,plain,
( t3least(X1842)
| equalish(u10r2(X1842),u9r2(X1842))
| equalish(u10r2(X1842),u10r1(X1842))
| equalish(u9r2(X1842),u10r1(X1842))
| s1most(X1842)
| r1most(X1842) ),
inference(resolution,[status(thm)],[c616,c40]) ).
cnf(c3034,plain,
( t3least(X1843)
| equalish(u10r2(X1843),u9r2(X1843))
| equalish(u9r2(X1843),u10r1(X1843))
| s1most(X1843)
| r1most(X1843) ),
inference(resolution,[status(thm)],[c1377,clause_39]) ).
cnf(c3162,plain,
( equalish(u10r2(X1846),u9r2(X1846))
| equalish(u9r2(X1846),u10r1(X1846))
| s1most(X1846)
| r1most(X1846)
| t(X1846,u8r2(X1846)) ),
inference(resolution,[status(thm)],[c3034,clause_31]) ).
cnf(c3112,plain,
( equalish(u10r2(X1845),u9r2(X1845))
| equalish(u9r2(X1845),u10r1(X1845))
| s1most(X1845)
| r1most(X1845)
| t(X1845,u8r3(X1845)) ),
inference(resolution,[status(thm)],[c3034,clause_32]) ).
cnf(c3057,plain,
( equalish(u10r2(X1844),u9r2(X1844))
| equalish(u9r2(X1844),u10r1(X1844))
| s1most(X1844)
| r1most(X1844)
| t(X1844,u8r1(X1844)) ),
inference(resolution,[status(thm)],[c3034,clause_30]) ).
cnf(c614,plain,
( t3least(X846)
| equalish(X847,u10r2(X846))
| equalish(X847,u10r1(X846))
| equalish(u10r2(X846),u10r1(X846))
| ~ t(X846,X847)
| s1most(X846) ),
inference(resolution,[status(thm)],[c90,c40]) ).
cnf(c1364,plain,
( t3least(X1766)
| equalish(u9r1(X1766),u10r2(X1766))
| equalish(u9r1(X1766),u10r1(X1766))
| equalish(u10r2(X1766),u10r1(X1766))
| s1most(X1766)
| r1most(X1766) ),
inference(resolution,[status(thm)],[c614,c15]) ).
cnf(c2672,plain,
( t3least(X1767)
| equalish(u9r1(X1767),u10r2(X1767))
| equalish(u9r1(X1767),u10r1(X1767))
| s1most(X1767)
| r1most(X1767) ),
inference(resolution,[status(thm)],[c1364,clause_39]) ).
cnf(c2800,plain,
( equalish(u9r1(X1770),u10r2(X1770))
| equalish(u9r1(X1770),u10r1(X1770))
| s1most(X1770)
| r1most(X1770)
| t(X1770,u8r2(X1770)) ),
inference(resolution,[status(thm)],[c2672,clause_31]) ).
cnf(c2750,plain,
( equalish(u9r1(X1769),u10r2(X1769))
| equalish(u9r1(X1769),u10r1(X1769))
| s1most(X1769)
| r1most(X1769)
| t(X1769,u8r3(X1769)) ),
inference(resolution,[status(thm)],[c2672,clause_32]) ).
cnf(c2695,plain,
( equalish(u9r1(X1768),u10r2(X1768))
| equalish(u9r1(X1768),u10r1(X1768))
| s1most(X1768)
| r1most(X1768)
| t(X1768,u8r1(X1768)) ),
inference(resolution,[status(thm)],[c2672,clause_30]) ).
cnf(c1363,plain,
( t3least(X1760)
| equalish(u9r2(X1760),u10r2(X1760))
| equalish(u9r2(X1760),u10r1(X1760))
| equalish(u10r2(X1760),u10r1(X1760))
| s1most(X1760)
| r1most(X1760) ),
inference(resolution,[status(thm)],[c614,c23]) ).
cnf(c2310,plain,
( t3least(X1761)
| equalish(u9r2(X1761),u10r2(X1761))
| equalish(u9r2(X1761),u10r1(X1761))
| s1most(X1761)
| r1most(X1761) ),
inference(resolution,[status(thm)],[c1363,clause_39]) ).
cnf(c2438,plain,
( equalish(u9r2(X1764),u10r2(X1764))
| equalish(u9r2(X1764),u10r1(X1764))
| s1most(X1764)
| r1most(X1764)
| t(X1764,u8r2(X1764)) ),
inference(resolution,[status(thm)],[c2310,clause_31]) ).
cnf(c2388,plain,
( equalish(u9r2(X1763),u10r2(X1763))
| equalish(u9r2(X1763),u10r1(X1763))
| s1most(X1763)
| r1most(X1763)
| t(X1763,u8r3(X1763)) ),
inference(resolution,[status(thm)],[c2310,clause_32]) ).
cnf(c2333,plain,
( equalish(u9r2(X1762),u10r2(X1762))
| equalish(u9r2(X1762),u10r1(X1762))
| s1most(X1762)
| r1most(X1762)
| t(X1762,u8r1(X1762)) ),
inference(resolution,[status(thm)],[c2310,clause_30]) ).
cnf(clause_5,axiom,
( p(X11,u1r1(X11))
| ~ p2least(X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(clause_2,axiom,
( p2least(X2)
| ~ c(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_17,axiom,
( c(X14)
| ~ r(X13,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_17) ).
cnf(c22,plain,
( r1most(X41)
| c(u9r2(X41)) ),
inference(resolution,[status(thm)],[clause_37,clause_17]) ).
cnf(c25,plain,
( r1most(X43)
| p2least(u9r2(X43)) ),
inference(resolution,[status(thm)],[c22,clause_2]) ).
cnf(c28,plain,
( r1most(X110)
| p(u9r2(X110),u1r1(u9r2(X110))) ),
inference(resolution,[status(thm)],[c25,clause_5]) ).
cnf(clause_10,axiom,
( equalish(X31,X33)
| ~ p1most(X32)
| ~ p(X32,X31)
| ~ p(X32,X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
cnf(clause_4,axiom,
( ~ p2least(X6)
| ~ equalish(u1r2(X6),u1r1(X6)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(clause_12,axiom,
( p1most(X22)
| p(X22,u3r1(X22)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_12) ).
cnf(clause_6,axiom,
( p(X17,u1r2(X17))
| ~ p2least(X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(c29,plain,
( r1most(X111)
| p(u9r2(X111),u1r2(u9r2(X111))) ),
inference(resolution,[status(thm)],[c25,clause_6]) ).
cnf(c187,plain,
( r1most(X414)
| equalish(X415,u1r1(u9r2(X414)))
| ~ p1most(u9r2(X414))
| ~ p(u9r2(X414),X415) ),
inference(resolution,[status(thm)],[c28,clause_10]) ).
cnf(c1141,plain,
( r1most(X452)
| equalish(u1r2(u9r2(X452)),u1r1(u9r2(X452)))
| ~ p1most(u9r2(X452)) ),
inference(resolution,[status(thm)],[c187,c29]) ).
cnf(c1171,plain,
( r1most(X1161)
| equalish(u1r2(u9r2(X1161)),u1r1(u9r2(X1161)))
| p(u9r2(X1161),u3r1(u9r2(X1161))) ),
inference(resolution,[status(thm)],[c1141,clause_12]) ).
cnf(c2059,plain,
( r1most(X1162)
| p(u9r2(X1162),u3r1(u9r2(X1162)))
| ~ p2least(u9r2(X1162)) ),
inference(resolution,[status(thm)],[c1171,clause_4]) ).
cnf(c2068,plain,
( r1most(X1163)
| p(u9r2(X1163),u3r1(u9r2(X1163))) ),
inference(resolution,[status(thm)],[c2059,c25]) ).
cnf(c2081,plain,
( r1most(X1198)
| equalish(X1199,u3r1(u9r2(X1198)))
| ~ p1most(u9r2(X1198))
| ~ p(u9r2(X1198),X1199) ),
inference(resolution,[status(thm)],[c2068,clause_10]) ).
cnf(c2157,plain,
( r1most(X1203)
| equalish(u1r1(u9r2(X1203)),u3r1(u9r2(X1203)))
| ~ p1most(u9r2(X1203)) ),
inference(resolution,[status(thm)],[c2081,c28]) ).
cnf(clause_13,axiom,
( p1most(X23)
| p(X23,u3r2(X23)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_13) ).
cnf(c1168,plain,
( r1most(X1109)
| equalish(u1r2(u9r2(X1109)),u1r1(u9r2(X1109)))
| p(u9r2(X1109),u3r2(u9r2(X1109))) ),
inference(resolution,[status(thm)],[c1141,clause_13]) ).
cnf(c1944,plain,
( r1most(X1110)
| p(u9r2(X1110),u3r2(u9r2(X1110)))
| ~ p2least(u9r2(X1110)) ),
inference(resolution,[status(thm)],[c1168,clause_4]) ).
cnf(c1952,plain,
( r1most(X1111)
| p(u9r2(X1111),u3r2(u9r2(X1111))) ),
inference(resolution,[status(thm)],[c1944,c25]) ).
cnf(c2153,plain,
( r1most(X1202)
| equalish(u3r2(u9r2(X1202)),u3r1(u9r2(X1202)))
| ~ p1most(u9r2(X1202)) ),
inference(resolution,[status(thm)],[c2081,c1952]) ).
cnf(c2149,plain,
( r1most(X1200)
| equalish(u1r2(u9r2(X1200)),u3r1(u9r2(X1200)))
| ~ p1most(u9r2(X1200)) ),
inference(resolution,[status(thm)],[c2081,c29]) ).
cnf(clause_25,axiom,
( e(X51)
| ~ a(u7r1(X51))
| ~ t3least(X51)
| ~ r1most(X51)
| ~ s1most(X51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_25) ).
cnf(clause_15,axiom,
( a(X7)
| ~ d(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
cnf(clause_16,axiom,
( a(X8)
| ~ c(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
cnf(clause_9,axiom,
( d(X5)
| ~ p1most(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
cnf(clause_3,axiom,
( c(X3)
| ~ p2least(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_11,axiom,
( p1most(X38)
| ~ equalish(u3r2(X38),u3r1(X38)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_11) ).
cnf(clause_7,axiom,
( p2least(X26)
| equalish(X25,X27)
| ~ p(X26,X25)
| ~ p(X26,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
cnf(c7,plain,
( p2least(X100)
| equalish(X101,u3r1(X100))
| ~ p(X100,X101)
| p1most(X100) ),
inference(resolution,[status(thm)],[clause_7,clause_12]) ).
cnf(c149,plain,
( p2least(X135)
| equalish(u3r2(X135),u3r1(X135))
| p1most(X135) ),
inference(resolution,[status(thm)],[c7,clause_13]) ).
cnf(c303,plain,
( p2least(X136)
| p1most(X136) ),
inference(resolution,[status(thm)],[c149,clause_11]) ).
cnf(c307,plain,
( p1most(X137)
| c(X137) ),
inference(resolution,[status(thm)],[c303,clause_3]) ).
cnf(c315,plain,
( c(X139)
| d(X139) ),
inference(resolution,[status(thm)],[c307,clause_9]) ).
cnf(c323,plain,
( d(X147)
| a(X147) ),
inference(resolution,[status(thm)],[c315,clause_16]) ).
cnf(c366,plain,
a(X148),
inference(resolution,[status(thm)],[c323,clause_15]) ).
cnf(c368,plain,
( e(X172)
| ~ t3least(X172)
| ~ r1most(X172)
| ~ s1most(X172) ),
inference(resolution,[status(thm)],[c366,clause_25]) ).
cnf(c429,plain,
( e(X221)
| ~ t3least(X221)
| ~ r1most(X221)
| s(X221,u10r2(X221)) ),
inference(resolution,[status(thm)],[c368,clause_41]) ).
cnf(c2076,plain,
( p(u9r2(X1197),u3r1(u9r2(X1197)))
| e(X1197)
| ~ t3least(X1197)
| s(X1197,u10r2(X1197)) ),
inference(resolution,[status(thm)],[c2068,c429]) ).
cnf(c434,plain,
( e(X223)
| ~ t3least(X223)
| ~ r1most(X223)
| t(X223,u10r1(X223)) ),
inference(resolution,[status(thm)],[c368,c34]) ).
cnf(c2072,plain,
( p(u9r2(X1196),u3r1(u9r2(X1196)))
| e(X1196)
| ~ t3least(X1196)
| t(X1196,u10r1(X1196)) ),
inference(resolution,[status(thm)],[c2068,c434]) ).
cnf(c431,plain,
( e(X222)
| ~ t3least(X222)
| ~ r1most(X222)
| t(X222,u10r2(X222)) ),
inference(resolution,[status(thm)],[c368,c40]) ).
cnf(c2071,plain,
( p(u9r2(X1195),u3r1(u9r2(X1195)))
| e(X1195)
| ~ t3least(X1195)
| t(X1195,u10r2(X1195)) ),
inference(resolution,[status(thm)],[c2068,c431]) ).
cnf(c435,plain,
( e(X224)
| ~ t3least(X224)
| ~ r1most(X224)
| s(X224,u10r1(X224)) ),
inference(resolution,[status(thm)],[c368,clause_40]) ).
cnf(c2070,plain,
( p(u9r2(X1192),u3r1(u9r2(X1192)))
| e(X1192)
| ~ t3least(X1192)
| s(X1192,u10r1(X1192)) ),
inference(resolution,[status(thm)],[c2068,c435]) ).
cnf(clause_19,axiom,
( d(X16)
| ~ s(X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
cnf(c39,plain,
( s1most(X54)
| d(u10r2(X54)) ),
inference(resolution,[status(thm)],[clause_41,clause_19]) ).
cnf(c433,plain,
( e(X218)
| ~ t3least(X218)
| ~ r1most(X218)
| d(u10r2(X218)) ),
inference(resolution,[status(thm)],[c368,c39]) ).
cnf(c2077,plain,
( p(u9r2(X1191),u3r1(u9r2(X1191)))
| e(X1191)
| ~ t3least(X1191)
| d(u10r2(X1191)) ),
inference(resolution,[status(thm)],[c2068,c433]) ).
cnf(clause_8,axiom,
( p1most(X4)
| ~ d(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_8) ).
cnf(c33,plain,
( s1most(X48)
| d(u10r1(X48)) ),
inference(resolution,[status(thm)],[clause_40,clause_19]) ).
cnf(c35,plain,
( s1most(X49)
| p1most(u10r1(X49)) ),
inference(resolution,[status(thm)],[c33,clause_8]) ).
cnf(c430,plain,
( e(X214)
| ~ t3least(X214)
| ~ r1most(X214)
| p1most(u10r1(X214)) ),
inference(resolution,[status(thm)],[c368,c35]) ).
cnf(c2075,plain,
( p(u9r2(X1190),u3r1(u9r2(X1190)))
| e(X1190)
| ~ t3least(X1190)
| p1most(u10r1(X1190)) ),
inference(resolution,[status(thm)],[c2068,c430]) ).
cnf(c41,plain,
( s1most(X55)
| p1most(u10r2(X55)) ),
inference(resolution,[status(thm)],[c39,clause_8]) ).
cnf(c436,plain,
( e(X219)
| ~ t3least(X219)
| ~ r1most(X219)
| p1most(u10r2(X219)) ),
inference(resolution,[status(thm)],[c368,c41]) ).
cnf(c2074,plain,
( p(u9r2(X1189),u3r1(u9r2(X1189)))
| e(X1189)
| ~ t3least(X1189)
| p1most(u10r2(X1189)) ),
inference(resolution,[status(thm)],[c2068,c436]) ).
cnf(c432,plain,
( e(X215)
| ~ t3least(X215)
| ~ r1most(X215)
| d(u10r1(X215)) ),
inference(resolution,[status(thm)],[c368,c33]) ).
cnf(c2073,plain,
( p(u9r2(X1188),u3r1(u9r2(X1188)))
| e(X1188)
| ~ t3least(X1188)
| d(u10r1(X1188)) ),
inference(resolution,[status(thm)],[c2068,c432]) ).
cnf(c193,plain,
( r1most(X437)
| equalish(X438,u1r2(u9r2(X437)))
| ~ p1most(u9r2(X437))
| ~ p(u9r2(X437),X438) ),
inference(resolution,[status(thm)],[c29,clause_10]) ).
cnf(c2083,plain,
( r1most(X1174)
| equalish(u3r1(u9r2(X1174)),u1r2(u9r2(X1174)))
| ~ p1most(u9r2(X1174)) ),
inference(resolution,[status(thm)],[c2068,c193]) ).
cnf(c1965,plain,
( r1most(X1143)
| equalish(X1144,u3r2(u9r2(X1143)))
| ~ p1most(u9r2(X1143))
| ~ p(u9r2(X1143),X1144) ),
inference(resolution,[status(thm)],[c1952,clause_10]) ).
cnf(c2082,plain,
( r1most(X1173)
| equalish(u3r1(u9r2(X1173)),u3r2(u9r2(X1173)))
| ~ p1most(u9r2(X1173)) ),
inference(resolution,[status(thm)],[c2068,c1965]) ).
cnf(c11,plain,
( equalish(X81,X81)
| ~ p1most(X80)
| ~ p(X80,X81) ),
inference(factor,[status(thm)],[clause_10]) ).
cnf(c2080,plain,
( r1most(X1170)
| equalish(u3r1(u9r2(X1170)),u3r1(u9r2(X1170)))
| ~ p1most(u9r2(X1170)) ),
inference(resolution,[status(thm)],[c2068,c11]) ).
cnf(c2078,plain,
( r1most(X1168)
| equalish(u3r1(u9r2(X1168)),u1r1(u9r2(X1168)))
| ~ p1most(u9r2(X1168)) ),
inference(resolution,[status(thm)],[c2068,c187]) ).
cnf(c2036,plain,
( r1most(X1147)
| equalish(u1r1(u9r2(X1147)),u3r2(u9r2(X1147)))
| ~ p1most(u9r2(X1147)) ),
inference(resolution,[status(thm)],[c1965,c28]) ).
cnf(c2027,plain,
( r1most(X1145)
| equalish(u1r2(u9r2(X1145)),u3r2(u9r2(X1145)))
| ~ p1most(u9r2(X1145)) ),
inference(resolution,[status(thm)],[c1965,c29]) ).
cnf(c1960,plain,
( p(u9r2(X1140),u3r2(u9r2(X1140)))
| e(X1140)
| ~ t3least(X1140)
| s(X1140,u10r2(X1140)) ),
inference(resolution,[status(thm)],[c1952,c429]) ).
cnf(c1956,plain,
( p(u9r2(X1139),u3r2(u9r2(X1139)))
| e(X1139)
| ~ t3least(X1139)
| t(X1139,u10r1(X1139)) ),
inference(resolution,[status(thm)],[c1952,c434]) ).
cnf(c1955,plain,
( p(u9r2(X1138),u3r2(u9r2(X1138)))
| e(X1138)
| ~ t3least(X1138)
| t(X1138,u10r2(X1138)) ),
inference(resolution,[status(thm)],[c1952,c431]) ).
cnf(c1954,plain,
( p(u9r2(X1137),u3r2(u9r2(X1137)))
| e(X1137)
| ~ t3least(X1137)
| s(X1137,u10r1(X1137)) ),
inference(resolution,[status(thm)],[c1952,c435]) ).
cnf(c1961,plain,
( p(u9r2(X1136),u3r2(u9r2(X1136)))
| e(X1136)
| ~ t3least(X1136)
| d(u10r2(X1136)) ),
inference(resolution,[status(thm)],[c1952,c433]) ).
cnf(c1959,plain,
( p(u9r2(X1133),u3r2(u9r2(X1133)))
| e(X1133)
| ~ t3least(X1133)
| p1most(u10r1(X1133)) ),
inference(resolution,[status(thm)],[c1952,c430]) ).
cnf(c1958,plain,
( p(u9r2(X1132),u3r2(u9r2(X1132)))
| e(X1132)
| ~ t3least(X1132)
| p1most(u10r2(X1132)) ),
inference(resolution,[status(thm)],[c1952,c436]) ).
cnf(c1957,plain,
( p(u9r2(X1131),u3r2(u9r2(X1131)))
| e(X1131)
| ~ t3least(X1131)
| d(u10r1(X1131)) ),
inference(resolution,[status(thm)],[c1952,c432]) ).
cnf(c1966,plain,
( r1most(X1122)
| equalish(u3r2(u9r2(X1122)),u1r2(u9r2(X1122)))
| ~ p1most(u9r2(X1122)) ),
inference(resolution,[status(thm)],[c1952,c193]) ).
cnf(c1964,plain,
( r1most(X1119)
| equalish(u3r2(u9r2(X1119)),u3r2(u9r2(X1119)))
| ~ p1most(u9r2(X1119)) ),
inference(resolution,[status(thm)],[c1952,c11]) ).
cnf(c1962,plain,
( r1most(X1117)
| equalish(u3r2(u9r2(X1117)),u1r1(u9r2(X1117)))
| ~ p1most(u9r2(X1117)) ),
inference(resolution,[status(thm)],[c1952,c187]) ).
cnf(c14,plain,
( r1most(X35)
| c(u9r1(X35)) ),
inference(resolution,[status(thm)],[clause_36,clause_17]) ).
cnf(c17,plain,
( r1most(X37)
| p2least(u9r1(X37)) ),
inference(resolution,[status(thm)],[c14,clause_2]) ).
cnf(c21,plain,
( r1most(X108)
| p(u9r1(X108),u1r2(u9r1(X108))) ),
inference(resolution,[status(thm)],[c17,clause_6]) ).
cnf(c20,plain,
( r1most(X107)
| p(u9r1(X107),u1r1(u9r1(X107))) ),
inference(resolution,[status(thm)],[c17,clause_5]) ).
cnf(c175,plain,
( r1most(X371)
| equalish(X370,u1r1(u9r1(X371)))
| ~ p1most(u9r1(X371))
| ~ p(u9r1(X371),X370) ),
inference(resolution,[status(thm)],[c20,clause_10]) ).
cnf(c912,plain,
( r1most(X434)
| equalish(u1r2(u9r1(X434)),u1r1(u9r1(X434)))
| ~ p1most(u9r1(X434)) ),
inference(resolution,[status(thm)],[c175,c21]) ).
cnf(c1146,plain,
( r1most(X979)
| equalish(u1r2(u9r1(X979)),u1r1(u9r1(X979)))
| p(u9r1(X979),u3r2(u9r1(X979))) ),
inference(resolution,[status(thm)],[c912,clause_13]) ).
cnf(c1682,plain,
( r1most(X980)
| p(u9r1(X980),u3r2(u9r1(X980)))
| ~ p2least(u9r1(X980)) ),
inference(resolution,[status(thm)],[c1146,clause_4]) ).
cnf(c1689,plain,
( r1most(X981)
| p(u9r1(X981),u3r2(u9r1(X981))) ),
inference(resolution,[status(thm)],[c1682,c17]) ).
cnf(c1149,plain,
( r1most(X1029)
| equalish(u1r2(u9r1(X1029)),u1r1(u9r1(X1029)))
| p(u9r1(X1029),u3r1(u9r1(X1029))) ),
inference(resolution,[status(thm)],[c912,clause_12]) ).
cnf(c1816,plain,
( r1most(X1030)
| p(u9r1(X1030),u3r1(u9r1(X1030)))
| ~ p2least(u9r1(X1030)) ),
inference(resolution,[status(thm)],[c1149,clause_4]) ).
cnf(c1824,plain,
( r1most(X1031)
| p(u9r1(X1031),u3r1(u9r1(X1031))) ),
inference(resolution,[status(thm)],[c1816,c17]) ).
cnf(c1839,plain,
( r1most(X1067)
| equalish(X1066,u3r1(u9r1(X1067)))
| ~ p1most(u9r1(X1067))
| ~ p(u9r1(X1067),X1066) ),
inference(resolution,[status(thm)],[c1824,clause_10]) ).
cnf(c1915,plain,
( r1most(X1072)
| equalish(u3r2(u9r1(X1072)),u3r1(u9r1(X1072)))
| ~ p1most(u9r1(X1072)) ),
inference(resolution,[status(thm)],[c1839,c1689]) ).
cnf(c1913,plain,
( r1most(X1071)
| equalish(u1r2(u9r1(X1071)),u3r1(u9r1(X1071)))
| ~ p1most(u9r1(X1071)) ),
inference(resolution,[status(thm)],[c1839,c21]) ).
cnf(c1910,plain,
( r1most(X1068)
| equalish(u1r1(u9r1(X1068)),u3r1(u9r1(X1068)))
| ~ p1most(u9r1(X1068)) ),
inference(resolution,[status(thm)],[c1839,c20]) ).
cnf(c1833,plain,
( p(u9r1(X1065),u3r1(u9r1(X1065)))
| e(X1065)
| ~ t3least(X1065)
| s(X1065,u10r2(X1065)) ),
inference(resolution,[status(thm)],[c1824,c429]) ).
cnf(c1829,plain,
( p(u9r1(X1064),u3r1(u9r1(X1064)))
| e(X1064)
| ~ t3least(X1064)
| t(X1064,u10r1(X1064)) ),
inference(resolution,[status(thm)],[c1824,c434]) ).
cnf(c1828,plain,
( p(u9r1(X1063),u3r1(u9r1(X1063)))
| e(X1063)
| ~ t3least(X1063)
| t(X1063,u10r2(X1063)) ),
inference(resolution,[status(thm)],[c1824,c431]) ).
cnf(c1827,plain,
( p(u9r1(X1060),u3r1(u9r1(X1060)))
| e(X1060)
| ~ t3least(X1060)
| s(X1060,u10r1(X1060)) ),
inference(resolution,[status(thm)],[c1824,c435]) ).
cnf(c1834,plain,
( p(u9r1(X1059),u3r1(u9r1(X1059)))
| e(X1059)
| ~ t3least(X1059)
| d(u10r2(X1059)) ),
inference(resolution,[status(thm)],[c1824,c433]) ).
cnf(c1832,plain,
( p(u9r1(X1058),u3r1(u9r1(X1058)))
| e(X1058)
| ~ t3least(X1058)
| p1most(u10r1(X1058)) ),
inference(resolution,[status(thm)],[c1824,c430]) ).
cnf(c1831,plain,
( p(u9r1(X1057),u3r1(u9r1(X1057)))
| e(X1057)
| ~ t3least(X1057)
| p1most(u10r2(X1057)) ),
inference(resolution,[status(thm)],[c1824,c436]) ).
cnf(c1830,plain,
( p(u9r1(X1056),u3r1(u9r1(X1056)))
| e(X1056)
| ~ t3least(X1056)
| d(u10r1(X1056)) ),
inference(resolution,[status(thm)],[c1824,c432]) ).
cnf(c1704,plain,
( r1most(X1008)
| equalish(X1009,u3r2(u9r1(X1008)))
| ~ p1most(u9r1(X1008))
| ~ p(u9r1(X1008),X1009) ),
inference(resolution,[status(thm)],[c1689,clause_10]) ).
cnf(c1841,plain,
( r1most(X1042)
| equalish(u3r1(u9r1(X1042)),u3r2(u9r1(X1042)))
| ~ p1most(u9r1(X1042)) ),
inference(resolution,[status(thm)],[c1824,c1704]) ).
cnf(c1838,plain,
( r1most(X1041)
| equalish(u3r1(u9r1(X1041)),u3r1(u9r1(X1041)))
| ~ p1most(u9r1(X1041)) ),
inference(resolution,[status(thm)],[c1824,c11]) ).
cnf(c1837,plain,
( r1most(X1038)
| equalish(u3r1(u9r1(X1038)),u1r1(u9r1(X1038)))
| ~ p1most(u9r1(X1038)) ),
inference(resolution,[status(thm)],[c1824,c175]) ).
cnf(c181,plain,
( r1most(X404)
| equalish(X403,u1r2(u9r1(X404)))
| ~ p1most(u9r1(X404))
| ~ p(u9r1(X404),X403) ),
inference(resolution,[status(thm)],[c21,clause_10]) ).
cnf(c1835,plain,
( r1most(X1036)
| equalish(u3r1(u9r1(X1036)),u1r2(u9r1(X1036)))
| ~ p1most(u9r1(X1036)) ),
inference(resolution,[status(thm)],[c1824,c181]) ).
cnf(c1791,plain,
( r1most(X1013)
| equalish(u1r2(u9r1(X1013)),u3r2(u9r1(X1013)))
| ~ p1most(u9r1(X1013)) ),
inference(resolution,[status(thm)],[c1704,c21]) ).
cnf(c1788,plain,
( r1most(X1012)
| equalish(u1r1(u9r1(X1012)),u3r2(u9r1(X1012)))
| ~ p1most(u9r1(X1012)) ),
inference(resolution,[status(thm)],[c1704,c20]) ).
cnf(c1698,plain,
( p(u9r1(X1007),u3r2(u9r1(X1007)))
| e(X1007)
| ~ t3least(X1007)
| s(X1007,u10r2(X1007)) ),
inference(resolution,[status(thm)],[c1689,c429]) ).
cnf(c1694,plain,
( p(u9r1(X1006),u3r2(u9r1(X1006)))
| e(X1006)
| ~ t3least(X1006)
| t(X1006,u10r1(X1006)) ),
inference(resolution,[status(thm)],[c1689,c434]) ).
cnf(c1693,plain,
( p(u9r1(X1005),u3r2(u9r1(X1005)))
| e(X1005)
| ~ t3least(X1005)
| t(X1005,u10r2(X1005)) ),
inference(resolution,[status(thm)],[c1689,c431]) ).
cnf(c1692,plain,
( p(u9r1(X1004),u3r2(u9r1(X1004)))
| e(X1004)
| ~ t3least(X1004)
| s(X1004,u10r1(X1004)) ),
inference(resolution,[status(thm)],[c1689,c435]) ).
cnf(c1699,plain,
( p(u9r1(X1001),u3r2(u9r1(X1001)))
| e(X1001)
| ~ t3least(X1001)
| d(u10r2(X1001)) ),
inference(resolution,[status(thm)],[c1689,c433]) ).
cnf(c1697,plain,
( p(u9r1(X1000),u3r2(u9r1(X1000)))
| e(X1000)
| ~ t3least(X1000)
| p1most(u10r1(X1000)) ),
inference(resolution,[status(thm)],[c1689,c430]) ).
cnf(c1696,plain,
( p(u9r1(X999),u3r2(u9r1(X999)))
| e(X999)
| ~ t3least(X999)
| p1most(u10r2(X999)) ),
inference(resolution,[status(thm)],[c1689,c436]) ).
cnf(c1695,plain,
( p(u9r1(X998),u3r2(u9r1(X998)))
| e(X998)
| ~ t3least(X998)
| d(u10r1(X998)) ),
inference(resolution,[status(thm)],[c1689,c432]) ).
cnf(c1703,plain,
( r1most(X989)
| equalish(u3r2(u9r1(X989)),u3r2(u9r1(X989)))
| ~ p1most(u9r1(X989)) ),
inference(resolution,[status(thm)],[c1689,c11]) ).
cnf(c1702,plain,
( r1most(X988)
| equalish(u3r2(u9r1(X988)),u1r1(u9r1(X988)))
| ~ p1most(u9r1(X988)) ),
inference(resolution,[status(thm)],[c1689,c175]) ).
cnf(c1700,plain,
( r1most(X986)
| equalish(u3r2(u9r1(X986)),u1r2(u9r1(X986)))
| ~ p1most(u9r1(X986)) ),
inference(resolution,[status(thm)],[c1689,c181]) ).
cnf(c703,plain,
( t3least(X945)
| equalish(X944,u9r1(X945))
| equalish(X944,u9r2(X945))
| equalish(u9r1(X945),u9r2(X945))
| ~ t(X945,X944)
| r1most(X945) ),
inference(resolution,[status(thm)],[c93,c15]) ).
cnf(c641,plain,
( t3least(X886)
| equalish(X885,u10r1(X886))
| equalish(X885,u10r2(X886))
| equalish(u10r1(X886),u10r2(X886))
| ~ t(X886,X885)
| s1most(X886) ),
inference(resolution,[status(thm)],[c91,c34]) ).
cnf(c563,plain,
( e(X541)
| ~ t3least(X541)
| s(X541,u10r1(X541))
| p(u9r1(X541),u1r1(u9r1(X541))) ),
inference(resolution,[status(thm)],[c435,c20]) ).
cnf(c556,plain,
( e(X540)
| ~ t3least(X540)
| s(X540,u10r1(X540))
| p(u9r2(X540),u1r1(u9r2(X540))) ),
inference(resolution,[status(thm)],[c435,c28]) ).
cnf(c555,plain,
( e(X539)
| ~ t3least(X539)
| s(X539,u10r1(X539))
| p(u9r1(X539),u1r2(u9r1(X539))) ),
inference(resolution,[status(thm)],[c435,c21]) ).
cnf(c554,plain,
( e(X538)
| ~ t3least(X538)
| s(X538,u10r1(X538))
| p(u9r2(X538),u1r2(u9r2(X538))) ),
inference(resolution,[status(thm)],[c435,c29]) ).
cnf(c550,plain,
( e(X536)
| ~ t3least(X536)
| t(X536,u10r1(X536))
| p(u9r1(X536),u1r1(u9r1(X536))) ),
inference(resolution,[status(thm)],[c434,c20]) ).
cnf(c543,plain,
( e(X535)
| ~ t3least(X535)
| t(X535,u10r1(X535))
| p(u9r2(X535),u1r1(u9r2(X535))) ),
inference(resolution,[status(thm)],[c434,c28]) ).
cnf(c542,plain,
( e(X534)
| ~ t3least(X534)
| t(X534,u10r1(X534))
| p(u9r1(X534),u1r2(u9r1(X534))) ),
inference(resolution,[status(thm)],[c434,c21]) ).
cnf(c541,plain,
( e(X533)
| ~ t3least(X533)
| t(X533,u10r1(X533))
| p(u9r2(X533),u1r2(u9r2(X533))) ),
inference(resolution,[status(thm)],[c434,c29]) ).
cnf(c537,plain,
( e(X532)
| ~ t3least(X532)
| t(X532,u10r2(X532))
| p(u9r1(X532),u1r1(u9r1(X532))) ),
inference(resolution,[status(thm)],[c431,c20]) ).
cnf(c530,plain,
( e(X530)
| ~ t3least(X530)
| t(X530,u10r2(X530))
| p(u9r2(X530),u1r1(u9r2(X530))) ),
inference(resolution,[status(thm)],[c431,c28]) ).
cnf(c529,plain,
( e(X529)
| ~ t3least(X529)
| t(X529,u10r2(X529))
| p(u9r1(X529),u1r2(u9r1(X529))) ),
inference(resolution,[status(thm)],[c431,c21]) ).
cnf(c528,plain,
( e(X528)
| ~ t3least(X528)
| t(X528,u10r2(X528))
| p(u9r2(X528),u1r2(u9r2(X528))) ),
inference(resolution,[status(thm)],[c431,c29]) ).
cnf(c524,plain,
( e(X527)
| ~ t3least(X527)
| s(X527,u10r2(X527))
| p(u9r1(X527),u1r1(u9r1(X527))) ),
inference(resolution,[status(thm)],[c429,c20]) ).
cnf(c517,plain,
( e(X526)
| ~ t3least(X526)
| s(X526,u10r2(X526))
| p(u9r2(X526),u1r1(u9r2(X526))) ),
inference(resolution,[status(thm)],[c429,c28]) ).
cnf(c516,plain,
( e(X525)
| ~ t3least(X525)
| s(X525,u10r2(X525))
| p(u9r1(X525),u1r2(u9r1(X525))) ),
inference(resolution,[status(thm)],[c429,c21]) ).
cnf(c515,plain,
( e(X524)
| ~ t3least(X524)
| s(X524,u10r2(X524))
| p(u9r2(X524),u1r2(u9r2(X524))) ),
inference(resolution,[status(thm)],[c429,c29]) ).
cnf(c511,plain,
( e(X481)
| ~ t3least(X481)
| p1most(u10r2(X481))
| p(u9r1(X481),u1r1(u9r1(X481))) ),
inference(resolution,[status(thm)],[c436,c20]) ).
cnf(c504,plain,
( e(X480)
| ~ t3least(X480)
| p1most(u10r2(X480))
| p(u9r2(X480),u1r1(u9r2(X480))) ),
inference(resolution,[status(thm)],[c436,c28]) ).
cnf(c503,plain,
( e(X479)
| ~ t3least(X479)
| p1most(u10r2(X479))
| p(u9r1(X479),u1r2(u9r1(X479))) ),
inference(resolution,[status(thm)],[c436,c21]) ).
cnf(c502,plain,
( e(X478)
| ~ t3least(X478)
| p1most(u10r2(X478))
| p(u9r2(X478),u1r2(u9r2(X478))) ),
inference(resolution,[status(thm)],[c436,c29]) ).
cnf(c498,plain,
( e(X477)
| ~ t3least(X477)
| d(u10r2(X477))
| p(u9r1(X477),u1r1(u9r1(X477))) ),
inference(resolution,[status(thm)],[c433,c20]) ).
cnf(c491,plain,
( e(X476)
| ~ t3least(X476)
| d(u10r2(X476))
| p(u9r2(X476),u1r1(u9r2(X476))) ),
inference(resolution,[status(thm)],[c433,c28]) ).
cnf(c490,plain,
( e(X475)
| ~ t3least(X475)
| d(u10r2(X475))
| p(u9r1(X475),u1r2(u9r1(X475))) ),
inference(resolution,[status(thm)],[c433,c21]) ).
cnf(c489,plain,
( e(X474)
| ~ t3least(X474)
| d(u10r2(X474))
| p(u9r2(X474),u1r2(u9r2(X474))) ),
inference(resolution,[status(thm)],[c433,c29]) ).
cnf(c485,plain,
( e(X473)
| ~ t3least(X473)
| d(u10r1(X473))
| p(u9r1(X473),u1r1(u9r1(X473))) ),
inference(resolution,[status(thm)],[c432,c20]) ).
cnf(c478,plain,
( e(X472)
| ~ t3least(X472)
| d(u10r1(X472))
| p(u9r2(X472),u1r1(u9r2(X472))) ),
inference(resolution,[status(thm)],[c432,c28]) ).
cnf(c477,plain,
( e(X470)
| ~ t3least(X470)
| d(u10r1(X470))
| p(u9r1(X470),u1r2(u9r1(X470))) ),
inference(resolution,[status(thm)],[c432,c21]) ).
cnf(c476,plain,
( e(X469)
| ~ t3least(X469)
| d(u10r1(X469))
| p(u9r2(X469),u1r2(u9r2(X469))) ),
inference(resolution,[status(thm)],[c432,c29]) ).
cnf(c472,plain,
( e(X468)
| ~ t3least(X468)
| p1most(u10r1(X468))
| p(u9r1(X468),u1r1(u9r1(X468))) ),
inference(resolution,[status(thm)],[c430,c20]) ).
cnf(c465,plain,
( e(X467)
| ~ t3least(X467)
| p1most(u10r1(X467))
| p(u9r2(X467),u1r1(u9r2(X467))) ),
inference(resolution,[status(thm)],[c430,c28]) ).
cnf(c464,plain,
( e(X466)
| ~ t3least(X466)
| p1most(u10r1(X466))
| p(u9r1(X466),u1r2(u9r1(X466))) ),
inference(resolution,[status(thm)],[c430,c21]) ).
cnf(c463,plain,
( e(X465)
| ~ t3least(X465)
| p1most(u10r1(X465))
| p(u9r2(X465),u1r2(u9r2(X465))) ),
inference(resolution,[status(thm)],[c430,c29]) ).
cnf(c1151,plain,
( r1most(X456)
| equalish(u1r1(u9r2(X456)),u1r2(u9r2(X456)))
| ~ p1most(u9r2(X456)) ),
inference(resolution,[status(thm)],[c193,c28]) ).
cnf(c1118,plain,
( r1most(X445)
| equalish(u1r1(u9r1(X445)),u1r2(u9r1(X445)))
| ~ p1most(u9r1(X445)) ),
inference(resolution,[status(thm)],[c181,c20]) ).
cnf(c192,plain,
( r1most(X412)
| equalish(u1r2(u9r2(X412)),u1r2(u9r2(X412)))
| ~ p1most(u9r2(X412)) ),
inference(resolution,[status(thm)],[c29,c11]) ).
cnf(c186,plain,
( r1most(X410)
| equalish(u1r1(u9r2(X410)),u1r1(u9r2(X410)))
| ~ p1most(u9r2(X410)) ),
inference(resolution,[status(thm)],[c28,c11]) ).
cnf(c180,plain,
( r1most(X402)
| equalish(u1r2(u9r1(X402)),u1r2(u9r1(X402)))
| ~ p1most(u9r1(X402)) ),
inference(resolution,[status(thm)],[c21,c11]) ).
cnf(c566,plain,
( e(X401)
| ~ t3least(X401)
| s(X401,u10r1(X401))
| t(X401,u9r2(X401)) ),
inference(resolution,[status(thm)],[c435,c23]) ).
cnf(c565,plain,
( e(X400)
| ~ t3least(X400)
| s(X400,u10r1(X400))
| r(X400,u9r1(X400)) ),
inference(resolution,[status(thm)],[c435,clause_36]) ).
cnf(c562,plain,
( e(X399)
| ~ t3least(X399)
| s(X399,u10r1(X399))
| t(X399,u9r1(X399)) ),
inference(resolution,[status(thm)],[c435,c15]) ).
cnf(c559,plain,
( e(X398)
| ~ t3least(X398)
| s(X398,u10r1(X398))
| r(X398,u9r2(X398)) ),
inference(resolution,[status(thm)],[c435,clause_37]) ).
cnf(c553,plain,
( e(X397)
| ~ t3least(X397)
| t(X397,u10r1(X397))
| t(X397,u9r2(X397)) ),
inference(resolution,[status(thm)],[c434,c23]) ).
cnf(c552,plain,
( e(X395)
| ~ t3least(X395)
| t(X395,u10r1(X395))
| r(X395,u9r1(X395)) ),
inference(resolution,[status(thm)],[c434,clause_36]) ).
cnf(c549,plain,
( e(X394)
| ~ t3least(X394)
| t(X394,u10r1(X394))
| t(X394,u9r1(X394)) ),
inference(resolution,[status(thm)],[c434,c15]) ).
cnf(c546,plain,
( e(X393)
| ~ t3least(X393)
| t(X393,u10r1(X393))
| r(X393,u9r2(X393)) ),
inference(resolution,[status(thm)],[c434,clause_37]) ).
cnf(c540,plain,
( e(X392)
| ~ t3least(X392)
| t(X392,u10r2(X392))
| t(X392,u9r2(X392)) ),
inference(resolution,[status(thm)],[c431,c23]) ).
cnf(c539,plain,
( e(X391)
| ~ t3least(X391)
| t(X391,u10r2(X391))
| r(X391,u9r1(X391)) ),
inference(resolution,[status(thm)],[c431,clause_36]) ).
cnf(c536,plain,
( e(X389)
| ~ t3least(X389)
| t(X389,u10r2(X389))
| t(X389,u9r1(X389)) ),
inference(resolution,[status(thm)],[c431,c15]) ).
cnf(c533,plain,
( e(X388)
| ~ t3least(X388)
| t(X388,u10r2(X388))
| r(X388,u9r2(X388)) ),
inference(resolution,[status(thm)],[c431,clause_37]) ).
cnf(c527,plain,
( e(X387)
| ~ t3least(X387)
| s(X387,u10r2(X387))
| t(X387,u9r2(X387)) ),
inference(resolution,[status(thm)],[c429,c23]) ).
cnf(c526,plain,
( e(X386)
| ~ t3least(X386)
| s(X386,u10r2(X386))
| r(X386,u9r1(X386)) ),
inference(resolution,[status(thm)],[c429,clause_36]) ).
cnf(c523,plain,
( e(X385)
| ~ t3least(X385)
| s(X385,u10r2(X385))
| t(X385,u9r1(X385)) ),
inference(resolution,[status(thm)],[c429,c15]) ).
cnf(c520,plain,
( e(X382)
| ~ t3least(X382)
| s(X382,u10r2(X382))
| r(X382,u9r2(X382)) ),
inference(resolution,[status(thm)],[c429,clause_37]) ).
cnf(c88,plain,
( t3least(X249)
| equalish(X250,X248)
| equalish(X250,X250)
| equalish(X248,X250)
| ~ t(X249,X250)
| ~ t(X249,X248) ),
inference(factor,[status(thm)],[clause_33]) ).
cnf(c567,plain,
( t3least(X251)
| equalish(X252,X252)
| ~ t(X251,X252) ),
inference(factor,[status(thm)],[c88]) ).
cnf(c579,plain,
( t3least(X259)
| equalish(u9r1(X259),u9r1(X259))
| r1most(X259) ),
inference(resolution,[status(thm)],[c567,c15]) ).
cnf(c603,plain,
( equalish(u9r1(X381),u9r1(X381))
| r1most(X381)
| t(X381,u8r3(X381)) ),
inference(resolution,[status(thm)],[c579,clause_32]) ).
cnf(c602,plain,
( equalish(u9r1(X380),u9r1(X380))
| r1most(X380)
| t(X380,u8r2(X380)) ),
inference(resolution,[status(thm)],[c579,clause_31]) ).
cnf(c601,plain,
( equalish(u9r1(X379),u9r1(X379))
| r1most(X379)
| t(X379,u8r1(X379)) ),
inference(resolution,[status(thm)],[c579,clause_30]) ).
cnf(c578,plain,
( t3least(X255)
| equalish(u9r2(X255),u9r2(X255))
| r1most(X255) ),
inference(resolution,[status(thm)],[c567,c23]) ).
cnf(c592,plain,
( equalish(u9r2(X378),u9r2(X378))
| r1most(X378)
| t(X378,u8r3(X378)) ),
inference(resolution,[status(thm)],[c578,clause_32]) ).
cnf(c591,plain,
( equalish(u9r2(X376),u9r2(X376))
| r1most(X376)
| t(X376,u8r2(X376)) ),
inference(resolution,[status(thm)],[c578,clause_31]) ).
cnf(c590,plain,
( equalish(u9r2(X375),u9r2(X375))
| r1most(X375)
| t(X375,u8r1(X375)) ),
inference(resolution,[status(thm)],[c578,clause_30]) ).
cnf(c576,plain,
( t3least(X254)
| equalish(u10r2(X254),u10r2(X254))
| s1most(X254) ),
inference(resolution,[status(thm)],[c567,c40]) ).
cnf(c588,plain,
( equalish(u10r2(X374),u10r2(X374))
| s1most(X374)
| t(X374,u8r3(X374)) ),
inference(resolution,[status(thm)],[c576,clause_32]) ).
cnf(c587,plain,
( equalish(u10r2(X373),u10r2(X373))
| s1most(X373)
| t(X373,u8r2(X373)) ),
inference(resolution,[status(thm)],[c576,clause_31]) ).
cnf(c586,plain,
( equalish(u10r2(X372),u10r2(X372))
| s1most(X372)
| t(X372,u8r1(X372)) ),
inference(resolution,[status(thm)],[c576,clause_30]) ).
cnf(c575,plain,
( t3least(X253)
| equalish(u10r1(X253),u10r1(X253))
| s1most(X253) ),
inference(resolution,[status(thm)],[c567,c34]) ).
cnf(c584,plain,
( equalish(u10r1(X369),u10r1(X369))
| s1most(X369)
| t(X369,u8r3(X369)) ),
inference(resolution,[status(thm)],[c575,clause_32]) ).
cnf(c583,plain,
( equalish(u10r1(X368),u10r1(X368))
| s1most(X368)
| t(X368,u8r2(X368)) ),
inference(resolution,[status(thm)],[c575,clause_31]) ).
cnf(c582,plain,
( equalish(u10r1(X367),u10r1(X367))
| s1most(X367)
| t(X367,u8r1(X367)) ),
inference(resolution,[status(thm)],[c575,clause_30]) ).
cnf(c564,plain,
( e(X366)
| ~ t3least(X366)
| s(X366,u10r1(X366))
| c(u9r2(X366)) ),
inference(resolution,[status(thm)],[c435,c22]) ).
cnf(c561,plain,
( e(X365)
| ~ t3least(X365)
| s(X365,u10r1(X365))
| c(u9r1(X365)) ),
inference(resolution,[status(thm)],[c435,c14]) ).
cnf(c174,plain,
( r1most(X364)
| equalish(u1r1(u9r1(X364)),u1r1(u9r1(X364)))
| ~ p1most(u9r1(X364)) ),
inference(resolution,[status(thm)],[c20,c11]) ).
cnf(c560,plain,
( e(X363)
| ~ t3least(X363)
| s(X363,u10r1(X363))
| p2least(u9r2(X363)) ),
inference(resolution,[status(thm)],[c435,c25]) ).
cnf(c557,plain,
( e(X362)
| ~ t3least(X362)
| s(X362,u10r1(X362))
| p2least(u9r1(X362)) ),
inference(resolution,[status(thm)],[c435,c17]) ).
cnf(c551,plain,
( e(X361)
| ~ t3least(X361)
| t(X361,u10r1(X361))
| c(u9r2(X361)) ),
inference(resolution,[status(thm)],[c434,c22]) ).
cnf(c548,plain,
( e(X360)
| ~ t3least(X360)
| t(X360,u10r1(X360))
| c(u9r1(X360)) ),
inference(resolution,[status(thm)],[c434,c14]) ).
cnf(c547,plain,
( e(X359)
| ~ t3least(X359)
| t(X359,u10r1(X359))
| p2least(u9r2(X359)) ),
inference(resolution,[status(thm)],[c434,c25]) ).
cnf(c544,plain,
( e(X357)
| ~ t3least(X357)
| t(X357,u10r1(X357))
| p2least(u9r1(X357)) ),
inference(resolution,[status(thm)],[c434,c17]) ).
cnf(c538,plain,
( e(X356)
| ~ t3least(X356)
| t(X356,u10r2(X356))
| c(u9r2(X356)) ),
inference(resolution,[status(thm)],[c431,c22]) ).
cnf(c535,plain,
( e(X355)
| ~ t3least(X355)
| t(X355,u10r2(X355))
| c(u9r1(X355)) ),
inference(resolution,[status(thm)],[c431,c14]) ).
cnf(c534,plain,
( e(X354)
| ~ t3least(X354)
| t(X354,u10r2(X354))
| p2least(u9r2(X354)) ),
inference(resolution,[status(thm)],[c431,c25]) ).
cnf(c531,plain,
( e(X353)
| ~ t3least(X353)
| t(X353,u10r2(X353))
| p2least(u9r1(X353)) ),
inference(resolution,[status(thm)],[c431,c17]) ).
cnf(c525,plain,
( e(X352)
| ~ t3least(X352)
| s(X352,u10r2(X352))
| c(u9r2(X352)) ),
inference(resolution,[status(thm)],[c429,c22]) ).
cnf(c522,plain,
( e(X351)
| ~ t3least(X351)
| s(X351,u10r2(X351))
| c(u9r1(X351)) ),
inference(resolution,[status(thm)],[c429,c14]) ).
cnf(c521,plain,
( e(X350)
| ~ t3least(X350)
| s(X350,u10r2(X350))
| p2least(u9r2(X350)) ),
inference(resolution,[status(thm)],[c429,c25]) ).
cnf(c518,plain,
( e(X349)
| ~ t3least(X349)
| s(X349,u10r2(X349))
| p2least(u9r1(X349)) ),
inference(resolution,[status(thm)],[c429,c17]) ).
cnf(c514,plain,
( e(X348)
| ~ t3least(X348)
| p1most(u10r2(X348))
| t(X348,u9r2(X348)) ),
inference(resolution,[status(thm)],[c436,c23]) ).
cnf(c513,plain,
( e(X347)
| ~ t3least(X347)
| p1most(u10r2(X347))
| r(X347,u9r1(X347)) ),
inference(resolution,[status(thm)],[c436,clause_36]) ).
cnf(c510,plain,
( e(X346)
| ~ t3least(X346)
| p1most(u10r2(X346))
| t(X346,u9r1(X346)) ),
inference(resolution,[status(thm)],[c436,c15]) ).
cnf(c507,plain,
( e(X345)
| ~ t3least(X345)
| p1most(u10r2(X345))
| r(X345,u9r2(X345)) ),
inference(resolution,[status(thm)],[c436,clause_37]) ).
cnf(c501,plain,
( e(X344)
| ~ t3least(X344)
| d(u10r2(X344))
| t(X344,u9r2(X344)) ),
inference(resolution,[status(thm)],[c433,c23]) ).
cnf(c500,plain,
( e(X343)
| ~ t3least(X343)
| d(u10r2(X343))
| r(X343,u9r1(X343)) ),
inference(resolution,[status(thm)],[c433,clause_36]) ).
cnf(c497,plain,
( e(X342)
| ~ t3least(X342)
| d(u10r2(X342))
| t(X342,u9r1(X342)) ),
inference(resolution,[status(thm)],[c433,c15]) ).
cnf(c494,plain,
( e(X341)
| ~ t3least(X341)
| d(u10r2(X341))
| r(X341,u9r2(X341)) ),
inference(resolution,[status(thm)],[c433,clause_37]) ).
cnf(c488,plain,
( e(X340)
| ~ t3least(X340)
| d(u10r1(X340))
| t(X340,u9r2(X340)) ),
inference(resolution,[status(thm)],[c432,c23]) ).
cnf(c487,plain,
( e(X339)
| ~ t3least(X339)
| d(u10r1(X339))
| r(X339,u9r1(X339)) ),
inference(resolution,[status(thm)],[c432,clause_36]) ).
cnf(c484,plain,
( e(X338)
| ~ t3least(X338)
| d(u10r1(X338))
| t(X338,u9r1(X338)) ),
inference(resolution,[status(thm)],[c432,c15]) ).
cnf(c481,plain,
( e(X337)
| ~ t3least(X337)
| d(u10r1(X337))
| r(X337,u9r2(X337)) ),
inference(resolution,[status(thm)],[c432,clause_37]) ).
cnf(c475,plain,
( e(X336)
| ~ t3least(X336)
| p1most(u10r1(X336))
| t(X336,u9r2(X336)) ),
inference(resolution,[status(thm)],[c430,c23]) ).
cnf(c474,plain,
( e(X335)
| ~ t3least(X335)
| p1most(u10r1(X335))
| r(X335,u9r1(X335)) ),
inference(resolution,[status(thm)],[c430,clause_36]) ).
cnf(c471,plain,
( e(X334)
| ~ t3least(X334)
| p1most(u10r1(X334))
| t(X334,u9r1(X334)) ),
inference(resolution,[status(thm)],[c430,c15]) ).
cnf(c468,plain,
( e(X333)
| ~ t3least(X333)
| p1most(u10r1(X333))
| r(X333,u9r2(X333)) ),
inference(resolution,[status(thm)],[c430,clause_37]) ).
cnf(c512,plain,
( e(X292)
| ~ t3least(X292)
| p1most(u10r2(X292))
| c(u9r2(X292)) ),
inference(resolution,[status(thm)],[c436,c22]) ).
cnf(c509,plain,
( e(X291)
| ~ t3least(X291)
| p1most(u10r2(X291))
| c(u9r1(X291)) ),
inference(resolution,[status(thm)],[c436,c14]) ).
cnf(c508,plain,
( e(X287)
| ~ t3least(X287)
| p1most(u10r2(X287))
| p2least(u9r2(X287)) ),
inference(resolution,[status(thm)],[c436,c25]) ).
cnf(c505,plain,
( e(X286)
| ~ t3least(X286)
| p1most(u10r2(X286))
| p2least(u9r1(X286)) ),
inference(resolution,[status(thm)],[c436,c17]) ).
cnf(c499,plain,
( e(X285)
| ~ t3least(X285)
| d(u10r2(X285))
| c(u9r2(X285)) ),
inference(resolution,[status(thm)],[c433,c22]) ).
cnf(c496,plain,
( e(X284)
| ~ t3least(X284)
| d(u10r2(X284))
| c(u9r1(X284)) ),
inference(resolution,[status(thm)],[c433,c14]) ).
cnf(c495,plain,
( e(X283)
| ~ t3least(X283)
| d(u10r2(X283))
| p2least(u9r2(X283)) ),
inference(resolution,[status(thm)],[c433,c25]) ).
cnf(c492,plain,
( e(X280)
| ~ t3least(X280)
| d(u10r2(X280))
| p2least(u9r1(X280)) ),
inference(resolution,[status(thm)],[c433,c17]) ).
cnf(c486,plain,
( e(X279)
| ~ t3least(X279)
| d(u10r1(X279))
| c(u9r2(X279)) ),
inference(resolution,[status(thm)],[c432,c22]) ).
cnf(c483,plain,
( e(X278)
| ~ t3least(X278)
| d(u10r1(X278))
| c(u9r1(X278)) ),
inference(resolution,[status(thm)],[c432,c14]) ).
cnf(c482,plain,
( e(X277)
| ~ t3least(X277)
| d(u10r1(X277))
| p2least(u9r2(X277)) ),
inference(resolution,[status(thm)],[c432,c25]) ).
cnf(c479,plain,
( e(X276)
| ~ t3least(X276)
| d(u10r1(X276))
| p2least(u9r1(X276)) ),
inference(resolution,[status(thm)],[c432,c17]) ).
cnf(c473,plain,
( e(X272)
| ~ t3least(X272)
| p1most(u10r1(X272))
| c(u9r2(X272)) ),
inference(resolution,[status(thm)],[c430,c22]) ).
cnf(c470,plain,
( e(X271)
| ~ t3least(X271)
| p1most(u10r1(X271))
| c(u9r1(X271)) ),
inference(resolution,[status(thm)],[c430,c14]) ).
cnf(c469,plain,
( e(X270)
| ~ t3least(X270)
| p1most(u10r1(X270))
| p2least(u9r2(X270)) ),
inference(resolution,[status(thm)],[c430,c25]) ).
cnf(c466,plain,
( e(X269)
| ~ t3least(X269)
| p1most(u10r1(X269))
| p2least(u9r1(X269)) ),
inference(resolution,[status(thm)],[c430,c17]) ).
cnf(c312,plain,
( p2least(X138)
| d(X138) ),
inference(resolution,[status(thm)],[c303,clause_9]) ).
cnf(c320,plain,
( d(X160)
| p(X160,u1r2(X160)) ),
inference(resolution,[status(thm)],[c312,clause_6]) ).
cnf(c319,plain,
( d(X159)
| p(X159,u1r1(X159)) ),
inference(resolution,[status(thm)],[c312,clause_5]) ).
cnf(c309,plain,
( p1most(X157)
| p(X157,u1r2(X157)) ),
inference(resolution,[status(thm)],[c303,clause_6]) ).
cnf(c308,plain,
( p1most(X156)
| p(X156,u1r1(X156)) ),
inference(resolution,[status(thm)],[c303,clause_5]) ).
cnf(clause_38,axiom,
( equalish(X93,X95)
| ~ s1most(X94)
| ~ s(X94,X93)
| ~ s(X94,X95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_38) ).
cnf(c116,plain,
( equalish(X97,X97)
| ~ s1most(X96)
| ~ s(X96,X97) ),
inference(factor,[status(thm)],[clause_38]) ).
cnf(clause_34,axiom,
( equalish(X86,X88)
| ~ r1most(X87)
| ~ r(X87,X86)
| ~ r(X87,X88) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_34) ).
cnf(c103,plain,
( equalish(X89,X89)
| ~ r1most(X90)
| ~ r(X90,X89) ),
inference(factor,[status(thm)],[clause_34]) ).
cnf(c5,plain,
( p2least(X75)
| equalish(X74,X74)
| ~ p(X75,X74) ),
inference(factor,[status(thm)],[clause_7]) ).
cnf(clause_29,axiom,
( ~ t3least(X71)
| ~ equalish(u8r3(X71),u8r2(X71)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_29) ).
cnf(clause_28,axiom,
( ~ t3least(X69)
| ~ equalish(u8r3(X69),u8r1(X69)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_28) ).
cnf(clause_27,axiom,
( ~ t3least(X63)
| ~ equalish(u8r2(X63),u8r1(X63)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_27) ).
cnf(c4,plain,
( p(X60,u3r2(X60))
| d(X60) ),
inference(resolution,[status(thm)],[clause_13,clause_9]) ).
cnf(c3,plain,
( p(X59,u3r1(X59))
| d(X59) ),
inference(resolution,[status(thm)],[clause_12,clause_9]) ).
cnf(clause_1,negated_conjecture,
e(exist),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(clause_23,axiom,
( t3least(X12)
| ~ e(X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
cnf(c2,plain,
t3least(exist),
inference(resolution,[status(thm)],[clause_23,clause_1]) ).
cnf(c10,plain,
t(exist,u8r3(exist)),
inference(resolution,[status(thm)],[clause_32,c2]) ).
cnf(c9,plain,
t(exist,u8r2(exist)),
inference(resolution,[status(thm)],[clause_31,c2]) ).
cnf(c8,plain,
t(exist,u8r1(exist)),
inference(resolution,[status(thm)],[clause_30,c2]) ).
cnf(clause_22,axiom,
( r1most(X10)
| ~ e(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_22) ).
cnf(c1,plain,
r1most(exist),
inference(resolution,[status(thm)],[clause_22,clause_1]) ).
cnf(clause_21,axiom,
( s1most(X9)
| ~ e(X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_21) ).
cnf(c0,plain,
s1most(exist),
inference(resolution,[status(thm)],[clause_21,clause_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS009-1 : TPTP v8.1.2. Released v2.0.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n020.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 9 00:05:53 EDT 2024
% 0.15/0.35 % CPUTime :
% 11.72/11.89 % Version: 1.5
% 11.72/11.89 % SZS status Satisfiable
% 11.72/11.89 % SZS output start Saturation
% See solution above
% 11.72/11.90
% 11.72/11.90 % Initial clauses : 41
% 11.72/11.90 % Processed clauses : 441
% 11.72/11.90 % Factors computed : 11
% 11.72/11.90 % Resolvents computed: 7956
% 11.72/11.90 % Tautologies deleted: 402
% 11.72/11.90 % Forward subsumed : 7165
% 11.72/11.90 % Backward subsumed : 91
% 11.72/11.90 % -------- CPU Time ---------
% 11.72/11.90 % User time : 11.485 s
% 11.72/11.90 % System time : 0.046 s
% 11.72/11.90 % Total time : 11.531 s
%------------------------------------------------------------------------------