%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN039-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:47:08 EDT 2024
% Result : Unsatisfiable 3.45s 3.67s
% Output : Refutation 3.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 12
% Syntax : Number of clauses : 46 ( 6 unt; 29 nHn; 7 RR)
% Number of literals : 126 ( 0 equ; 31 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% Number of variables : 170 ( 79 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(c_2,negated_conjecture,
( p(f1(X37,X38),f1(X37,X38))
| ~ s(X37,f1(X37,X38))
| q(f1(X37,X38),X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_2) ).
cnf(c_5,negated_conjecture,
( p(f1(X99,X100),f1(X99,X100))
| s(f1(X99,X100),X101)
| q(f1(X99,X100),X98) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_5) ).
cnf(c_19,negated_conjecture,
( s(X58,X56)
| ~ s(X56,f1(X56,X57))
| ~ q(X57,f1(X56,X57)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_19) ).
cnf(c_26,negated_conjecture,
( s(X35,X33)
| ~ q(X32,X32)
| q(f1(X33,X34),X32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_26) ).
cnf(c_20,negated_conjecture,
( s(X62,X60)
| ~ s(X60,f1(X60,X61))
| q(f1(X60,X61),X59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_20) ).
cnf(c46,plain,
( p(f1(X997,X998),f1(X997,X998))
| q(f1(X997,X998),X1001)
| s(X996,f1(X997,X998))
| q(f1(f1(X997,X998),X999),X1000) ),
inference(resolution,[status(thm)],[c_5,c_20]) ).
cnf(c1399,plain,
( p(f1(X4436,X4439),f1(X4436,X4439))
| q(f1(X4436,X4439),X4438)
| q(f1(f1(X4436,X4439),X4437),X4440)
| q(f1(X4436,X4439),X4441) ),
inference(resolution,[status(thm)],[c46,c_2]) ).
cnf(c2185,plain,
( p(f1(X4449,X4451),f1(X4449,X4451))
| q(f1(X4449,X4451),X4450)
| q(f1(f1(X4449,X4451),X4448),X4452) ),
inference(factor,[status(thm)],[c1399]) ).
cnf(c2306,plain,
( p(f1(X4740,X4744),f1(X4740,X4744))
| q(f1(X4740,X4744),X4739)
| s(X4741,X4738)
| q(f1(X4738,X4742),f1(f1(X4740,X4744),X4743)) ),
inference(resolution,[status(thm)],[c2185,c_26]) ).
cnf(c2515,plain,
( p(f1(X4749,X4750),f1(X4749,X4750))
| q(f1(X4749,X4750),f1(f1(X4749,X4750),X4751))
| s(X4748,X4749) ),
inference(factor,[status(thm)],[c2306]) ).
cnf(c2606,plain,
( p(f1(X6960,X6959),f1(X6960,X6959))
| s(X6962,X6960)
| s(X6961,f1(X6960,X6959))
| ~ s(f1(X6960,X6959),f1(f1(X6960,X6959),f1(X6960,X6959))) ),
inference(resolution,[status(thm)],[c2515,c_19]) ).
cnf(c4945,plain,
( p(f1(X6968,X6969),f1(X6968,X6969))
| s(X6971,X6968)
| s(X6970,f1(X6968,X6969))
| q(f1(X6968,X6969),X6972) ),
inference(resolution,[status(thm)],[c2606,c_5]) ).
cnf(c5015,plain,
( p(f1(X6977,X6979),f1(X6977,X6979))
| s(X6981,X6977)
| q(f1(X6977,X6979),X6978)
| q(f1(X6977,X6979),X6980) ),
inference(resolution,[status(thm)],[c4945,c_2]) ).
cnf(c5124,plain,
( p(f1(X6982,X6985),f1(X6982,X6985))
| s(X6984,X6982)
| q(f1(X6982,X6985),X6983) ),
inference(factor,[status(thm)],[c5015]) ).
cnf(c_25,negated_conjecture,
( s(X31,X29)
| ~ q(X28,X28)
| ~ q(X30,f1(X29,X30)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_25) ).
cnf(c5382,plain,
( p(f1(X6997,X6999),f1(X6997,X6999))
| s(X7001,X6997)
| s(X7002,X7000)
| ~ q(X6998,X6998) ),
inference(resolution,[status(thm)],[c5124,c_25]) ).
cnf(c5416,plain,
( p(f1(X7319,X7318),f1(X7319,X7318))
| s(X7317,X7319)
| s(X7316,X7315)
| p(f1(X7313,X7314),f1(X7313,X7314))
| s(X7320,X7313) ),
inference(resolution,[status(thm)],[c5382,c5124]) ).
cnf(c6035,plain,
( p(f1(X7322,X7325),f1(X7322,X7325))
| s(X7323,X7322)
| s(X7326,X7321)
| s(X7324,X7322) ),
inference(factor,[status(thm)],[c5416]) ).
cnf(c6186,plain,
( p(f1(X7329,X7330),f1(X7329,X7330))
| s(X7328,X7329)
| s(X7327,X7329) ),
inference(factor,[status(thm)],[c6035]) ).
cnf(c6315,plain,
( p(f1(X7340,X7339),f1(X7340,X7339))
| s(X7341,X7340) ),
inference(factor,[status(thm)],[c6186]) ).
cnf(c_3,negated_conjecture,
( p(f1(X54,X55),f1(X54,X55))
| ~ s(X54,f1(X54,X55))
| ~ s(X55,X55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_3) ).
cnf(c_21,negated_conjecture,
( s(X24,X22)
| ~ s(X22,f1(X22,X23))
| ~ s(X23,X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_21) ).
cnf(c_6,negated_conjecture,
( p(f1(X84,X85),f1(X84,X85))
| s(f1(X84,X85),X86)
| ~ s(X85,X85) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_6) ).
cnf(c6451,plain,
( p(f1(X7590,X7591),f1(X7590,X7591))
| p(f1(X7588,X7590),f1(X7588,X7590))
| s(f1(X7588,X7590),X7589) ),
inference(resolution,[status(thm)],[c6315,c_6]) ).
cnf(c6990,plain,
( p(f1(X7593,X7593),f1(X7593,X7593))
| s(f1(X7593,X7593),X7592) ),
inference(factor,[status(thm)],[c6451]) ).
cnf(c7086,plain,
( p(f1(X7606,X7606),f1(X7606,X7606))
| s(X7607,f1(X7606,X7606))
| ~ s(X7608,X7608) ),
inference(resolution,[status(thm)],[c6990,c_21]) ).
cnf(c7124,plain,
( p(f1(X7724,X7724),f1(X7724,X7724))
| s(X7725,f1(X7724,X7724))
| p(f1(X7723,X7722),f1(X7723,X7722)) ),
inference(resolution,[status(thm)],[c7086,c6315]) ).
cnf(c7603,plain,
( p(f1(X7736,X7736),f1(X7736,X7736))
| s(X7735,f1(X7736,X7736)) ),
inference(factor,[status(thm)],[c7124]) ).
cnf(c7725,plain,
( p(f1(X7737,X7737),f1(X7737,X7737))
| ~ s(X7737,X7737) ),
inference(resolution,[status(thm)],[c7603,c_3]) ).
cnf(c7746,plain,
( p(f1(X7771,X7771),f1(X7771,X7771))
| p(f1(X7771,X7772),f1(X7771,X7772)) ),
inference(resolution,[status(thm)],[c7725,c6315]) ).
cnf(c7834,plain,
p(f1(X7773,X7773),f1(X7773,X7773)),
inference(factor,[status(thm)],[c7746]) ).
cnf(c_14,negated_conjecture,
( ~ p(X51,X51)
| s(f1(X51,X52),X53)
| q(f1(X51,X52),X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_14) ).
cnf(c7875,plain,
( s(f1(f1(X7774,X7774),X7776),X7775)
| q(f1(f1(X7774,X7774),X7776),X7777) ),
inference(resolution,[status(thm)],[c7834,c_14]) ).
cnf(c_16,negated_conjecture,
( ~ p(X15,X15)
| ~ q(X14,X14)
| ~ q(X16,f1(X15,X16)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_16) ).
cnf(c7934,plain,
( s(f1(f1(X7800,X7800),X7801),X7799)
| ~ p(X7797,X7797)
| ~ q(X7798,X7798) ),
inference(resolution,[status(thm)],[c7875,c_16]) ).
cnf(c8045,plain,
( s(f1(f1(X8028,X8028),X8026),X8023)
| ~ p(X8025,X8025)
| s(f1(f1(X8027,X8027),X8029),X8024) ),
inference(resolution,[status(thm)],[c7934,c7875]) ).
cnf(c8515,plain,
( s(f1(f1(X8033,X8033),X8035),X8034)
| s(f1(f1(X8032,X8032),X8030),X8031) ),
inference(resolution,[status(thm)],[c8045,c7834]) ).
cnf(c8519,plain,
s(f1(f1(X8038,X8038),X8037),X8036),
inference(factor,[status(thm)],[c8515]) ).
cnf(c8598,plain,
( s(X8051,f1(f1(X8052,X8052),X8050))
| ~ s(X8053,X8053) ),
inference(resolution,[status(thm)],[c8519,c_21]) ).
cnf(c8689,plain,
s(X8054,f1(f1(X8055,X8055),X8056)),
inference(resolution,[status(thm)],[c8598,c8519]) ).
cnf(c8713,plain,
( s(X8058,f1(X8057,X8057))
| ~ s(X8059,X8059) ),
inference(resolution,[status(thm)],[c8689,c_21]) ).
cnf(c8737,plain,
s(X8060,f1(X8061,X8061)),
inference(resolution,[status(thm)],[c8713,c8689]) ).
cnf(c_12,negated_conjecture,
( ~ p(X9,X9)
| ~ s(X9,f1(X9,X10))
| ~ s(X10,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_12) ).
cnf(c8775,plain,
( ~ p(X8070,X8070)
| ~ s(X8070,X8070) ),
inference(resolution,[status(thm)],[c8737,c_12]) ).
cnf(c8809,plain,
~ p(f1(X8075,X8075),f1(X8075,X8075)),
inference(resolution,[status(thm)],[c8775,c8737]) ).
cnf(c8885,plain,
$false,
inference(resolution,[status(thm)],[c8809,c7834]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN039-1 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:56:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 3.45/3.67 % Version: 1.5
% 3.45/3.67 % SZS status Unsatisfiable
% 3.45/3.67 % SZS output start CNFRefutation
% See solution above
% 3.45/3.67
% 3.45/3.67 % Initial clauses : 27
% 3.45/3.67 % Processed clauses : 332
% 3.45/3.67 % Factors computed : 82
% 3.45/3.67 % Resolvents computed: 8807
% 3.45/3.67 % Tautologies deleted: 14
% 3.45/3.67 % Forward subsumed : 1056
% 3.45/3.67 % Backward subsumed : 239
% 3.45/3.67 % -------- CPU Time ---------
% 3.45/3.67 % User time : 3.270 s
% 3.45/3.67 % System time : 0.028 s
% 3.45/3.67 % Total time : 3.298 s
%------------------------------------------------------------------------------