%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN092-1.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:21 EDT 2024
% Result : Satisfiable 0.53s 0.68s
% Output : Saturation 0.53s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(sym_s3_type2_3,axiom,
( ~ sym_q_5
| sym_q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type2_3) ).
cnf(sym_s3_type12_7,axiom,
( ~ sym_q_3
| sym_p_4
| sym_q_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_7) ).
cnf(sym_s3_type12_6,axiom,
( ~ sym_q_2
| sym_q_3
| sym_p_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_6) ).
cnf(sym_s3_type11_6,axiom,
( ~ sym_p_2
| sym_q_3
| sym_q_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_6) ).
cnf(sym_s3_type11_4,axiom,
( ~ sym_p_1
| sym_q_2
| sym_q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_4) ).
cnf(sym_s3_type12_1,axiom,
( ~ sym_q_0
| sym_p_1
| sym_q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_1) ).
cnf(sym_s3_goal_1,axiom,
( sym_p_0
| sym_q_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_goal_1) ).
cnf(sym_s3_type11_1,axiom,
( ~ sym_p_0
| sym_p_1
| sym_p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_1) ).
cnf(c0,plain,
( sym_p_1
| sym_p_2
| sym_q_0 ),
inference(resolution,[status(thm)],[sym_s3_type11_1,sym_s3_goal_1]) ).
cnf(c8,plain,
( sym_p_1
| sym_p_2
| sym_q_2 ),
inference(resolution,[status(thm)],[c0,sym_s3_type12_1]) ).
cnf(c42,plain,
( sym_p_2
| sym_q_2
| sym_q_3 ),
inference(resolution,[status(thm)],[c8,sym_s3_type11_4]) ).
cnf(c107,plain,
( sym_q_2
| sym_q_3
| sym_q_4 ),
inference(resolution,[status(thm)],[c42,sym_s3_type11_6]) ).
cnf(c167,plain,
( sym_q_3
| sym_q_4
| sym_p_4 ),
inference(resolution,[status(thm)],[c107,sym_s3_type12_6]) ).
cnf(c226,plain,
( sym_q_4
| sym_p_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c167,sym_s3_type12_7]) ).
cnf(c279,plain,
( sym_q_4
| sym_p_4
| sym_q_2 ),
inference(resolution,[status(thm)],[c226,sym_s3_type2_3]) ).
cnf(sym_s3_type2_1,axiom,
( ~ sym_p_5
| sym_p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type2_1) ).
cnf(sym_s3_type12_8,axiom,
( ~ sym_q_3
| sym_q_4
| sym_p_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_8) ).
cnf(c225,plain,
( sym_q_4
| sym_p_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c167,sym_s3_type12_8]) ).
cnf(c278,plain,
( sym_q_4
| sym_p_4
| sym_p_2 ),
inference(resolution,[status(thm)],[c225,sym_s3_type2_1]) ).
cnf(sym_s3_type11_8,axiom,
( ~ sym_p_3
| sym_q_4
| sym_q_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_8) ).
cnf(sym_s3_type12_3,axiom,
( ~ sym_q_1
| sym_p_2
| sym_q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_3) ).
cnf(sym_s3_type12_2,axiom,
( ~ sym_q_0
| sym_q_1
| sym_p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_2) ).
cnf(sym_s3_type11_3,axiom,
( ~ sym_p_1
| sym_p_2
| sym_p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_3) ).
cnf(c5,plain,
( sym_p_2
| sym_q_0
| sym_p_3 ),
inference(resolution,[status(thm)],[c0,sym_s3_type11_3]) ).
cnf(c31,plain,
( sym_p_2
| sym_p_3
| sym_q_1 ),
inference(resolution,[status(thm)],[c5,sym_s3_type12_2]) ).
cnf(c104,plain,
( sym_p_2
| sym_p_3
| sym_q_3 ),
inference(resolution,[status(thm)],[c31,sym_s3_type12_3]) ).
cnf(c162,plain,
( sym_p_3
| sym_q_3
| sym_q_4 ),
inference(resolution,[status(thm)],[c104,sym_s3_type11_6]) ).
cnf(c221,plain,
( sym_q_3
| sym_q_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c162,sym_s3_type11_8]) ).
cnf(c272,plain,
( sym_q_4
| sym_q_5
| sym_p_5 ),
inference(resolution,[status(thm)],[c221,sym_s3_type12_8]) ).
cnf(sym_s3_type11_7,axiom,
( ~ sym_p_3
| sym_p_4
| sym_p_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_7) ).
cnf(sym_s3_type11_5,axiom,
( ~ sym_p_2
| sym_p_3
| sym_p_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_5) ).
cnf(c161,plain,
( sym_p_3
| sym_q_3
| sym_p_4 ),
inference(resolution,[status(thm)],[c104,sym_s3_type11_5]) ).
cnf(c218,plain,
( sym_q_3
| sym_p_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c161,sym_s3_type11_7]) ).
cnf(c267,plain,
( sym_p_4
| sym_p_5
| sym_q_5 ),
inference(resolution,[status(thm)],[c218,sym_s3_type12_7]) ).
cnf(sym_s3_type11_2,axiom,
( ~ sym_p_0
| sym_q_1
| sym_q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type11_2) ).
cnf(c1,plain,
( sym_q_1
| sym_q_2
| sym_q_0 ),
inference(resolution,[status(thm)],[sym_s3_type11_2,sym_s3_goal_1]) ).
cnf(c14,plain,
( sym_q_1
| sym_q_2
| sym_p_1 ),
inference(resolution,[status(thm)],[c1,sym_s3_type12_1]) ).
cnf(c64,plain,
( sym_q_1
| sym_q_2
| sym_q_3 ),
inference(resolution,[status(thm)],[c14,sym_s3_type11_4]) ).
cnf(c142,plain,
( sym_q_1
| sym_q_3
| sym_p_4 ),
inference(resolution,[status(thm)],[c64,sym_s3_type12_6]) ).
cnf(c203,plain,
( sym_q_1
| sym_p_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c142,sym_s3_type12_7]) ).
cnf(c253,plain,
( sym_q_1
| sym_p_4
| sym_q_2 ),
inference(resolution,[status(thm)],[c203,sym_s3_type2_3]) ).
cnf(sym_s3_type12_5,axiom,
( ~ sym_q_2
| sym_p_3
| sym_q_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_5) ).
cnf(sym_s3_type12_4,axiom,
( ~ sym_q_1
| sym_q_2
| sym_p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type12_4) ).
cnf(c11,plain,
( sym_q_2
| sym_q_0
| sym_p_3 ),
inference(resolution,[status(thm)],[c1,sym_s3_type12_4]) ).
cnf(c55,plain,
( sym_q_0
| sym_p_3
| sym_q_4 ),
inference(resolution,[status(thm)],[c11,sym_s3_type12_5]) ).
cnf(c126,plain,
( sym_q_0
| sym_q_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c55,sym_s3_type11_8]) ).
cnf(c189,plain,
( sym_q_0
| sym_q_4
| sym_q_2 ),
inference(resolution,[status(thm)],[c126,sym_s3_type2_3]) ).
cnf(c244,plain,
( sym_q_4
| sym_q_2
| sym_p_1 ),
inference(resolution,[status(thm)],[c189,sym_s3_type12_1]) ).
cnf(c9,plain,
( sym_p_1
| sym_p_2
| sym_q_1 ),
inference(resolution,[status(thm)],[c0,sym_s3_type12_2]) ).
cnf(c52,plain,
( sym_p_1
| sym_p_2
| sym_q_3 ),
inference(resolution,[status(thm)],[c9,sym_s3_type12_3]) ).
cnf(c121,plain,
( sym_p_1
| sym_q_3
| sym_q_4 ),
inference(resolution,[status(thm)],[c52,sym_s3_type11_6]) ).
cnf(c185,plain,
( sym_p_1
| sym_q_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c121,sym_s3_type12_8]) ).
cnf(c243,plain,
( sym_p_1
| sym_q_4
| sym_p_2 ),
inference(resolution,[status(thm)],[c185,sym_s3_type2_1]) ).
cnf(c108,plain,
( sym_p_2
| sym_q_3
| sym_p_4 ),
inference(resolution,[status(thm)],[c42,sym_s3_type12_6]) ).
cnf(c174,plain,
( sym_p_2
| sym_p_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c108,sym_s3_type12_7]) ).
cnf(c232,plain,
( sym_p_2
| sym_p_4
| sym_q_2 ),
inference(resolution,[status(thm)],[c174,sym_s3_type2_3]) ).
cnf(c169,plain,
( sym_q_2
| sym_q_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c107,sym_s3_type12_8]) ).
cnf(c229,plain,
( sym_q_2
| sym_q_4
| sym_p_2 ),
inference(resolution,[status(thm)],[c169,sym_s3_type2_1]) ).
cnf(c223,plain,
( sym_p_3
| sym_q_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c162,sym_s3_type12_8]) ).
cnf(c220,plain,
( sym_p_3
| sym_p_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c161,sym_s3_type12_7]) ).
cnf(c28,plain,
( sym_q_0
| sym_p_3
| sym_p_4 ),
inference(resolution,[status(thm)],[c5,sym_s3_type11_5]) ).
cnf(c99,plain,
( sym_q_0
| sym_p_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c28,sym_s3_type11_7]) ).
cnf(c156,plain,
( sym_q_0
| sym_p_4
| sym_p_2 ),
inference(resolution,[status(thm)],[c99,sym_s3_type2_1]) ).
cnf(c211,plain,
( sym_p_4
| sym_p_2
| sym_q_1 ),
inference(resolution,[status(thm)],[c156,sym_s3_type12_2]) ).
cnf(c3,plain,
( sym_q_1
| sym_p_2
| sym_p_0 ),
inference(resolution,[status(thm)],[sym_s3_type12_2,sym_s3_goal_1]) ).
cnf(c22,plain,
( sym_p_2
| sym_p_0
| sym_q_3 ),
inference(resolution,[status(thm)],[c3,sym_s3_type12_3]) ).
cnf(c85,plain,
( sym_p_0
| sym_q_3
| sym_q_4 ),
inference(resolution,[status(thm)],[c22,sym_s3_type11_6]) ).
cnf(c152,plain,
( sym_p_0
| sym_q_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c85,sym_s3_type12_8]) ).
cnf(c209,plain,
( sym_p_0
| sym_q_4
| sym_p_2 ),
inference(resolution,[status(thm)],[c152,sym_s3_type2_1]) ).
cnf(c2,plain,
( sym_p_1
| sym_q_2
| sym_p_0 ),
inference(resolution,[status(thm)],[sym_s3_type12_1,sym_s3_goal_1]) ).
cnf(c16,plain,
( sym_q_2
| sym_p_0
| sym_q_3 ),
inference(resolution,[status(thm)],[c2,sym_s3_type11_4]) ).
cnf(c78,plain,
( sym_p_0
| sym_q_3
| sym_p_4 ),
inference(resolution,[status(thm)],[c16,sym_s3_type12_6]) ).
cnf(c149,plain,
( sym_p_0
| sym_p_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c78,sym_s3_type12_7]) ).
cnf(c206,plain,
( sym_p_0
| sym_p_4
| sym_q_2 ),
inference(resolution,[status(thm)],[c149,sym_s3_type2_3]) ).
cnf(c56,plain,
( sym_q_2
| sym_p_3
| sym_p_1 ),
inference(resolution,[status(thm)],[c11,sym_s3_type12_1]) ).
cnf(c129,plain,
( sym_p_3
| sym_p_1
| sym_q_4 ),
inference(resolution,[status(thm)],[c56,sym_s3_type12_5]) ).
cnf(c190,plain,
( sym_p_1
| sym_q_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c129,sym_s3_type11_8]) ).
cnf(c43,plain,
( sym_p_2
| sym_q_2
| sym_p_3 ),
inference(resolution,[status(thm)],[c8,sym_s3_type11_3]) ).
cnf(c115,plain,
( sym_p_2
| sym_p_3
| sym_q_4 ),
inference(resolution,[status(thm)],[c43,sym_s3_type12_5]) ).
cnf(c181,plain,
( sym_p_2
| sym_q_4
| sym_q_5 ),
inference(resolution,[status(thm)],[c115,sym_s3_type11_8]) ).
cnf(c112,plain,
( sym_q_2
| sym_p_3
| sym_p_4 ),
inference(resolution,[status(thm)],[c43,sym_s3_type11_5]) ).
cnf(c178,plain,
( sym_q_2
| sym_p_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c112,sym_s3_type11_7]) ).
cnf(c176,plain,
( sym_p_3
| sym_p_4
| sym_q_4 ),
inference(resolution,[status(thm)],[c112,sym_s3_type12_5]) ).
cnf(c100,plain,
( sym_p_3
| sym_q_1
| sym_p_4 ),
inference(resolution,[status(thm)],[c31,sym_s3_type11_5]) ).
cnf(c158,plain,
( sym_q_1
| sym_p_4
| sym_p_5 ),
inference(resolution,[status(thm)],[c100,sym_s3_type11_7]) ).
cnf(c132,plain,
( sym_q_2
| sym_p_3
| sym_q_3 ),
inference(resolution,[status(thm)],[c56,sym_s3_type11_4]) ).
cnf(c15,plain,
( sym_q_1
| sym_q_2
| sym_p_2 ),
inference(resolution,[status(thm)],[c1,sym_s3_type12_2]) ).
cnf(s3_type12_8,axiom,
( q_3
| ~ q_4
| ~ p_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_8) ).
cnf(s3_type12_7,axiom,
( q_3
| ~ p_4
| ~ q_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_7) ).
cnf(s3_type12_6,axiom,
( q_2
| ~ q_3
| ~ p_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_6) ).
cnf(s3_type12_5,axiom,
( q_2
| ~ p_3
| ~ q_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_5) ).
cnf(s3_type12_4,axiom,
( q_1
| ~ q_2
| ~ p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_4) ).
cnf(s3_type12_3,axiom,
( q_1
| ~ p_2
| ~ q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_3) ).
cnf(s3_type12_2,axiom,
( q_0
| ~ q_1
| ~ p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_2) ).
cnf(s3_type12_1,axiom,
( q_0
| ~ p_1
| ~ q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type12_1) ).
cnf(s3_type11_8,axiom,
( p_3
| ~ q_4
| ~ q_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_8) ).
cnf(s3_type11_7,axiom,
( p_3
| ~ p_4
| ~ p_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_7) ).
cnf(s3_type11_6,axiom,
( p_2
| ~ q_3
| ~ q_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_6) ).
cnf(s3_type11_5,axiom,
( p_2
| ~ p_3
| ~ p_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_5) ).
cnf(s3_type11_4,axiom,
( p_1
| ~ q_2
| ~ q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_4) ).
cnf(s3_type11_3,axiom,
( p_1
| ~ p_2
| ~ p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_3) ).
cnf(s3_type11_2,axiom,
( p_0
| ~ q_1
| ~ q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_2) ).
cnf(sym_s3_type2_4,axiom,
( ~ sym_q_6
| sym_q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type2_4) ).
cnf(sym_s3_type2_2,axiom,
( ~ sym_p_6
| sym_p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_s3_type2_2) ).
cnf(s3_type11_1,axiom,
( p_0
| ~ p_1
| ~ p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type11_1) ).
cnf(s3_type2_4,axiom,
( q_6
| ~ q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type2_4) ).
cnf(s3_type2_3,axiom,
( q_5
| ~ q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type2_3) ).
cnf(s3_type2_2,axiom,
( p_6
| ~ p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type2_2) ).
cnf(s3_type2_1,axiom,
( p_5
| ~ p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_type2_1) ).
cnf(s3_goal_1,negated_conjecture,
( ~ p_0
| ~ q_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_goal_1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN092-1.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:02:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.53/0.68 % Version: 1.5
% 0.53/0.68 % SZS status Satisfiable
% 0.53/0.68 % SZS output start Saturation
% See solution above
% 0.53/0.69
% 0.53/0.69 % Initial clauses : 42
% 0.53/0.69 % Processed clauses : 114
% 0.53/0.69 % Factors computed : 0
% 0.53/0.69 % Resolvents computed: 308
% 0.53/0.69 % Tautologies deleted: 0
% 0.53/0.69 % Forward subsumed : 236
% 0.53/0.69 % Backward subsumed : 4
% 0.53/0.69 % -------- CPU Time ---------
% 0.53/0.69 % User time : 0.323 s
% 0.53/0.69 % System time : 0.016 s
% 0.53/0.69 % Total time : 0.339 s
%------------------------------------------------------------------------------