%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR040+2 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:18:15 EDT 2024
% Result : Theorem 3.04s 3.28s
% Output : Refutation 3.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 21
% Syntax : Number of formulae : 103 ( 23 unt; 0 def)
% Number of atoms : 183 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 147 ( 67 ~; 57 |; 2 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 76 ( 0 sgn 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1_475,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_475) ).
cnf(c1988,plain,
firstordercollection(c_tptpcol_16_62187),
inference(split_conjunct,[status(thm)],[ax1_475]) ).
fof(ax1_205,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_205) ).
fof(c2479,plain,
! [OBJ] :
( ~ firstordercollection(OBJ)
| fixedordercollection(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_205]) ).
fof(c2480,plain,
! [X1033] :
( ~ firstordercollection(X1033)
| fixedordercollection(X1033) ),
inference(variable_rename,[status(thm)],[c2479]) ).
cnf(c2481,plain,
( ~ firstordercollection(X1404)
| fixedordercollection(X1404) ),
inference(split_conjunct,[status(thm)],[c2480]) ).
cnf(c3828,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2481,c1988]) ).
fof(ax1_151,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_151) ).
fof(c2582,plain,
! [OBJ] :
( ~ fixedordercollection(OBJ)
| collection(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_151]) ).
fof(c2583,plain,
! [X1055] :
( ~ fixedordercollection(X1055)
| collection(X1055) ),
inference(variable_rename,[status(thm)],[c2582]) ).
cnf(c2584,plain,
( ~ fixedordercollection(X1514)
| collection(X1514) ),
inference(split_conjunct,[status(thm)],[c2583]) ).
cnf(c4259,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2584,c3828]) ).
fof(ax1_289,axiom,
! [OBJ] :
~ ( collection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_289) ).
fof(c2326,plain,
! [OBJ] :
( ~ collection(OBJ)
| ~ individual(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_289]) ).
fof(c2327,plain,
! [X999] :
( ~ collection(X999)
| ~ individual(X999) ),
inference(variable_rename,[status(thm)],[c2326]) ).
cnf(c2328,plain,
( ~ collection(X1344)
| ~ individual(X1344) ),
inference(split_conjunct,[status(thm)],[c2327]) ).
fof(ax1_445,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_445) ).
fof(c2040,plain,
! [OBJ] :
( ~ tptpcol_0_0(OBJ)
| individual(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_445]) ).
fof(c2041,plain,
! [X926] :
( ~ tptpcol_0_0(X926)
| individual(X926) ),
inference(variable_rename,[status(thm)],[c2040]) ).
cnf(c2042,plain,
( ~ tptpcol_0_0(X1188)
| individual(X1188) ),
inference(split_conjunct,[status(thm)],[c2041]) ).
fof(ax1_124,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_124) ).
fof(c2628,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| tptpcol_0_0(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_124]) ).
fof(c2629,plain,
! [X1067] :
( ~ tptpcol_1_65536(X1067)
| tptpcol_0_0(X1067) ),
inference(variable_rename,[status(thm)],[c2628]) ).
cnf(c2630,plain,
( ~ tptpcol_1_65536(X1534)
| tptpcol_0_0(X1534) ),
inference(split_conjunct,[status(thm)],[c2629]) ).
fof(ax1_234,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_234) ).
fof(c2426,plain,
! [OBJ] :
( ~ tptpcol_3_98305(OBJ)
| tptpcol_2_98304(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_234]) ).
fof(c2427,plain,
! [X1021] :
( ~ tptpcol_3_98305(X1021)
| tptpcol_2_98304(X1021) ),
inference(variable_rename,[status(thm)],[c2426]) ).
cnf(c2428,plain,
( ~ tptpcol_3_98305(X1385)
| tptpcol_2_98304(X1385) ),
inference(split_conjunct,[status(thm)],[c2427]) ).
fof(ax1_117,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_117) ).
fof(c2641,plain,
! [OBJ] :
( ~ tptpcol_5_106498(OBJ)
| tptpcol_4_106497(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_117]) ).
fof(c2642,plain,
! [X1069] :
( ~ tptpcol_5_106498(X1069)
| tptpcol_4_106497(X1069) ),
inference(variable_rename,[status(thm)],[c2641]) ).
cnf(c2643,plain,
( ~ tptpcol_5_106498(X1539)
| tptpcol_4_106497(X1539) ),
inference(split_conjunct,[status(thm)],[c2642]) ).
fof(ax1_459,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_459) ).
fof(c2018,plain,
! [OBJ] :
( ~ tptpcol_6_108546(OBJ)
| tptpcol_5_106498(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_459]) ).
fof(c2019,plain,
! [X923] :
( ~ tptpcol_6_108546(X923)
| tptpcol_5_106498(X923) ),
inference(variable_rename,[status(thm)],[c2018]) ).
cnf(c2020,plain,
( ~ tptpcol_6_108546(X1181)
| tptpcol_5_106498(X1181) ),
inference(split_conjunct,[status(thm)],[c2019]) ).
fof(ax1_341,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_341) ).
fof(c2235,plain,
! [OBJ] :
( ~ tptpcol_7_108547(OBJ)
| tptpcol_6_108546(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_341]) ).
fof(c2236,plain,
! [X977] :
( ~ tptpcol_7_108547(X977)
| tptpcol_6_108546(X977) ),
inference(variable_rename,[status(thm)],[c2235]) ).
cnf(c2237,plain,
( ~ tptpcol_7_108547(X1302)
| tptpcol_6_108546(X1302) ),
inference(split_conjunct,[status(thm)],[c2236]) ).
fof(ax1_185,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_185) ).
fof(c2517,plain,
! [OBJ] :
( ~ tptpcol_8_109059(OBJ)
| tptpcol_7_108547(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_185]) ).
fof(c2518,plain,
! [X1041] :
( ~ tptpcol_8_109059(X1041)
| tptpcol_7_108547(X1041) ),
inference(variable_rename,[status(thm)],[c2517]) ).
cnf(c2519,plain,
( ~ tptpcol_8_109059(X1418)
| tptpcol_7_108547(X1418) ),
inference(split_conjunct,[status(thm)],[c2518]) ).
fof(ax1_242,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_242) ).
fof(c2410,plain,
! [OBJ] :
( ~ tptpcol_9_109060(OBJ)
| tptpcol_8_109059(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_242]) ).
fof(c2411,plain,
! [X1017] :
( ~ tptpcol_9_109060(X1017)
| tptpcol_8_109059(X1017) ),
inference(variable_rename,[status(thm)],[c2410]) ).
cnf(c2412,plain,
( ~ tptpcol_9_109060(X1378)
| tptpcol_8_109059(X1378) ),
inference(split_conjunct,[status(thm)],[c2411]) ).
fof(ax1_343,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_343) ).
fof(c2231,plain,
! [OBJ] :
( ~ tptpcol_11_109125(OBJ)
| tptpcol_10_109061(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_343]) ).
fof(c2232,plain,
! [X976] :
( ~ tptpcol_11_109125(X976)
| tptpcol_10_109061(X976) ),
inference(variable_rename,[status(thm)],[c2231]) ).
cnf(c2233,plain,
( ~ tptpcol_11_109125(X1301)
| tptpcol_10_109061(X1301) ),
inference(split_conjunct,[status(thm)],[c2232]) ).
fof(ax1_360,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_360) ).
fof(c2201,plain,
! [OBJ] :
( ~ tptpcol_12_109157(OBJ)
| tptpcol_11_109125(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_360]) ).
fof(c2202,plain,
! [X970] :
( ~ tptpcol_12_109157(X970)
| tptpcol_11_109125(X970) ),
inference(variable_rename,[status(thm)],[c2201]) ).
cnf(c2203,plain,
( ~ tptpcol_12_109157(X1277)
| tptpcol_11_109125(X1277) ),
inference(split_conjunct,[status(thm)],[c2202]) ).
fof(query90,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query90) ).
fof(c0,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(assume_negation,[status(cth)],[query90]) ).
fof(c1,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(fof_simplification,[status(thm)],[c0]) ).
fof(c2,negated_conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
& tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(fof_nnf,[status(thm)],[c1]) ).
cnf(c4,negated_conjecture,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(split_conjunct,[status(thm)],[c2]) ).
fof(ax1_266,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_266) ).
fof(c2367,plain,
! [OBJ] :
( ~ tptpcol_15_109185(OBJ)
| tptpcol_14_109181(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_266]) ).
fof(c2368,plain,
! [X1008] :
( ~ tptpcol_15_109185(X1008)
| tptpcol_14_109181(X1008) ),
inference(variable_rename,[status(thm)],[c2367]) ).
cnf(c2369,plain,
( ~ tptpcol_15_109185(X1363)
| tptpcol_14_109181(X1363) ),
inference(split_conjunct,[status(thm)],[c2368]) ).
cnf(c3648,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2369,c4]) ).
fof(ax1_251,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_251) ).
fof(c2396,plain,
! [OBJ] :
( ~ tptpcol_14_109181(OBJ)
| tptpcol_13_109173(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_251]) ).
fof(c2397,plain,
! [X1015] :
( ~ tptpcol_14_109181(X1015)
| tptpcol_13_109173(X1015) ),
inference(variable_rename,[status(thm)],[c2396]) ).
cnf(c2398,plain,
( ~ tptpcol_14_109181(X1375)
| tptpcol_13_109173(X1375) ),
inference(split_conjunct,[status(thm)],[c2397]) ).
cnf(c3698,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2398,c3648]) ).
fof(ax1_114,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_114) ).
fof(c2646,plain,
! [OBJ] :
( ~ tptpcol_13_109173(OBJ)
| tptpcol_12_109157(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_114]) ).
fof(c2647,plain,
! [X1070] :
( ~ tptpcol_13_109173(X1070)
| tptpcol_12_109157(X1070) ),
inference(variable_rename,[status(thm)],[c2646]) ).
cnf(c2648,plain,
( ~ tptpcol_13_109173(X1546)
| tptpcol_12_109157(X1546) ),
inference(split_conjunct,[status(thm)],[c2647]) ).
cnf(c4381,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2648,c3698]) ).
cnf(c4382,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4381,c2203]) ).
cnf(c4383,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4382,c2233]) ).
fof(ax1_96,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_96) ).
fof(c2682,plain,
! [OBJ] :
( ~ tptpcol_10_109061(OBJ)
| tptpcol_9_109060(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_96]) ).
fof(c2683,plain,
! [X1080] :
( ~ tptpcol_10_109061(X1080)
| tptpcol_9_109060(X1080) ),
inference(variable_rename,[status(thm)],[c2682]) ).
cnf(c2684,plain,
( ~ tptpcol_10_109061(X1559)
| tptpcol_9_109060(X1559) ),
inference(split_conjunct,[status(thm)],[c2683]) ).
cnf(c4424,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2684,c4383]) ).
cnf(c4425,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4424,c2412]) ).
cnf(c4426,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4425,c2519]) ).
cnf(c4427,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4426,c2237]) ).
cnf(c4428,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4427,c2020]) ).
cnf(c4429,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4428,c2643]) ).
fof(ax1_69,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_69) ).
fof(c2730,plain,
! [OBJ] :
( ~ tptpcol_4_106497(OBJ)
| tptpcol_3_98305(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_69]) ).
fof(c2731,plain,
! [X1089] :
( ~ tptpcol_4_106497(X1089)
| tptpcol_3_98305(X1089) ),
inference(variable_rename,[status(thm)],[c2730]) ).
cnf(c2732,plain,
( ~ tptpcol_4_106497(X1584)
| tptpcol_3_98305(X1584) ),
inference(split_conjunct,[status(thm)],[c2731]) ).
cnf(c4531,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2732,c4429]) ).
cnf(c4533,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4531,c2428]) ).
fof(ax1_50,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_50) ).
fof(c2760,plain,
! [OBJ] :
( ~ tptpcol_2_98304(OBJ)
| tptpcol_1_65536(OBJ) ),
inference(fof_nnf,[status(thm)],[ax1_50]) ).
fof(c2761,plain,
! [X1099] :
( ~ tptpcol_2_98304(X1099)
| tptpcol_1_65536(X1099) ),
inference(variable_rename,[status(thm)],[c2760]) ).
cnf(c2762,plain,
( ~ tptpcol_2_98304(X1597)
| tptpcol_1_65536(X1597) ),
inference(split_conjunct,[status(thm)],[c2761]) ).
cnf(c4620,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c2762,c4533]) ).
cnf(c4621,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4620,c2630]) ).
cnf(c4624,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4621,c2042]) ).
cnf(c4626,plain,
~ collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c4624,c2328]) ).
cnf(c4628,plain,
$false,
inference(resolution,[status(thm)],[c4626,c4259]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR040+2 : TPTP v8.1.2. Released v3.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n006.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 01:40:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 3.04/3.28 % Version: 1.5
% 3.04/3.28 % SZS status Theorem
% 3.04/3.28 % SZS output start CNFRefutation
% See solution above
% 3.04/3.28
% 3.04/3.28 % Initial clauses : 1133
% 3.04/3.28 % Processed clauses : 1113
% 3.04/3.28 % Factors computed : 6
% 3.04/3.28 % Resolvents computed: 1768
% 3.04/3.28 % Tautologies deleted: 0
% 3.04/3.28 % Forward subsumed : 189
% 3.04/3.28 % Backward subsumed : 0
% 3.04/3.28 % -------- CPU Time ---------
% 3.04/3.28 % User time : 2.909 s
% 3.04/3.28 % System time : 0.020 s
% 3.04/3.28 % Total time : 2.929 s
%------------------------------------------------------------------------------