%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN091-1.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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.44s 0.58s
% Output : Saturation 0.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(sym_s2_type11_6,axiom,
( ~ sym_p_2_3
| sym_q_3_3
| sym_q_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type11_6) ).
cnf(sym_s2_type12_2,axiom,
( ~ sym_q_1_2
| sym_q_2_2
| sym_p_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type12_2) ).
cnf(sym_s2_type22_2,axiom,
( ~ sym_p_3_3
| sym_p_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type22_2) ).
cnf(sym_s2_type22_3,axiom,
( ~ sym_q_2_2
| sym_q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type22_3) ).
cnf(sym_s2_goal_1,axiom,
sym_p_1_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_goal_1) ).
cnf(sym_s2_type11_4,axiom,
( ~ sym_p_1_3
| sym_q_2_3
| sym_q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type11_4) ).
cnf(c1,plain,
( sym_q_2_3
| sym_q_1_2 ),
inference(resolution,[status(thm)],[sym_s2_type11_4,sym_s2_goal_1]) ).
cnf(sym_s2_type12_5,axiom,
( ~ sym_q_2_3
| sym_p_3_3
| sym_q_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type12_5) ).
cnf(c8,plain,
( sym_p_3_3
| sym_q_2_2
| sym_q_1_2 ),
inference(resolution,[status(thm)],[sym_s2_type12_5,c1]) ).
cnf(c38,plain,
( sym_p_3_3
| sym_q_1_2 ),
inference(resolution,[status(thm)],[c8,sym_s2_type22_3]) ).
cnf(c41,plain,
( sym_q_1_2
| sym_p_2_3 ),
inference(resolution,[status(thm)],[c38,sym_s2_type22_2]) ).
cnf(c44,plain,
( sym_p_2_3
| sym_q_2_2
| sym_p_1_1 ),
inference(resolution,[status(thm)],[c41,sym_s2_type12_2]) ).
cnf(c94,plain,
( sym_q_2_2
| sym_p_1_1
| sym_q_3_3 ),
inference(resolution,[status(thm)],[c44,sym_s2_type11_6]) ).
cnf(sym_s2_type22_1,axiom,
( ~ sym_p_2_2
| sym_p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type22_1) ).
cnf(sym_s2_type12_6,axiom,
( ~ sym_q_2_3
| sym_q_3_3
| sym_p_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type12_6) ).
cnf(sym_s2_type12_1,axiom,
( ~ sym_q_1_2
| sym_p_2_2
| sym_q_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type12_1) ).
cnf(c6,plain,
( sym_p_2_2
| sym_q_1_1
| sym_q_2_3 ),
inference(resolution,[status(thm)],[sym_s2_type12_1,c1]) ).
cnf(c31,plain,
( sym_p_2_2
| sym_q_1_1
| sym_q_3_3 ),
inference(resolution,[status(thm)],[c6,sym_s2_type12_6]) ).
cnf(c84,plain,
( sym_q_1_1
| sym_q_3_3
| sym_p_1_2 ),
inference(resolution,[status(thm)],[c31,sym_s2_type22_1]) ).
cnf(sym_s2_type22_4,axiom,
( ~ sym_q_3_3
| sym_q_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type22_4) ).
cnf(sym_s2_type11_2,axiom,
( ~ sym_p_1_2
| sym_q_2_2
| sym_q_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type11_2) ).
cnf(sym_s2_type11_3,axiom,
( ~ sym_p_1_3
| sym_p_2_3
| sym_p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type11_3) ).
cnf(c0,plain,
( sym_p_2_3
| sym_p_1_2 ),
inference(resolution,[status(thm)],[sym_s2_type11_3,sym_s2_goal_1]) ).
cnf(c2,plain,
( sym_p_2_3
| sym_q_2_2
| sym_q_1_1 ),
inference(resolution,[status(thm)],[c0,sym_s2_type11_2]) ).
cnf(c11,plain,
( sym_q_2_2
| sym_q_1_1
| sym_q_3_3 ),
inference(resolution,[status(thm)],[c2,sym_s2_type11_6]) ).
cnf(c54,plain,
( sym_q_2_2
| sym_q_1_1
| sym_q_2_3 ),
inference(resolution,[status(thm)],[c11,sym_s2_type22_4]) ).
cnf(c47,plain,
( sym_q_1_2
| sym_q_3_3
| sym_q_2_2 ),
inference(resolution,[status(thm)],[c41,sym_s2_type11_6]) ).
cnf(c104,plain,
( sym_q_1_2
| sym_q_3_3 ),
inference(resolution,[status(thm)],[c47,sym_s2_type22_3]) ).
cnf(c45,plain,
( sym_p_2_3
| sym_p_2_2
| sym_q_1_1 ),
inference(resolution,[status(thm)],[c41,sym_s2_type12_1]) ).
cnf(c43,plain,
( sym_p_3_3
| sym_p_2_2
| sym_q_1_1 ),
inference(resolution,[status(thm)],[c38,sym_s2_type12_1]) ).
cnf(c7,plain,
( sym_q_2_2
| sym_p_1_1
| sym_q_2_3 ),
inference(resolution,[status(thm)],[sym_s2_type12_2,c1]) ).
cnf(c36,plain,
( sym_q_2_2
| sym_p_1_1
| sym_p_3_3 ),
inference(resolution,[status(thm)],[c7,sym_s2_type12_5]) ).
cnf(c29,plain,
( sym_q_1_1
| sym_q_2_3
| sym_p_1_2 ),
inference(resolution,[status(thm)],[c6,sym_s2_type22_1]) ).
cnf(c5,plain,
( sym_q_3_3
| sym_q_2_2
| sym_p_1_2 ),
inference(resolution,[status(thm)],[sym_s2_type11_6,c0]) ).
cnf(c25,plain,
( sym_q_2_2
| sym_p_1_2
| sym_q_2_3 ),
inference(resolution,[status(thm)],[c5,sym_s2_type22_4]) ).
cnf(sym_s2_type11_5,axiom,
( ~ sym_p_2_3
| sym_p_3_3
| sym_p_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type11_5) ).
cnf(c4,plain,
( sym_p_3_3
| sym_p_2_2
| sym_p_1_2 ),
inference(resolution,[status(thm)],[sym_s2_type11_5,c0]) ).
cnf(c19,plain,
( sym_p_3_3
| sym_p_1_2 ),
inference(resolution,[status(thm)],[c4,sym_s2_type22_1]) ).
cnf(c23,plain,
( sym_p_3_3
| sym_q_2_2
| sym_q_1_1 ),
inference(resolution,[status(thm)],[c19,sym_s2_type11_2]) ).
cnf(sym_s2_type11_1,axiom,
( ~ sym_p_1_2
| sym_p_2_2
| sym_p_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type11_1) ).
cnf(c3,plain,
( sym_p_2_3
| sym_p_2_2
| sym_p_1_1 ),
inference(resolution,[status(thm)],[c0,sym_s2_type11_1]) ).
cnf(c14,plain,
( sym_p_2_2
| sym_p_1_1
| sym_p_3_3 ),
inference(resolution,[status(thm)],[c3,sym_s2_type11_5]) ).
cnf(sym_s2_type12_4,axiom,
( ~ sym_q_1_3
| sym_q_2_3
| sym_p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type12_4) ).
cnf(s2_type12_6,axiom,
( q_2_3
| ~ q_3_3
| ~ p_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type12_6) ).
cnf(s2_type12_5,axiom,
( q_2_3
| ~ p_3_3
| ~ q_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type12_5) ).
cnf(s2_type12_4,axiom,
( q_1_3
| ~ q_2_3
| ~ p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type12_4) ).
cnf(s2_type12_3,axiom,
( q_1_3
| ~ p_2_3
| ~ q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type12_3) ).
cnf(s2_type12_2,axiom,
( q_1_2
| ~ q_2_2
| ~ p_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type12_2) ).
cnf(s2_type12_1,axiom,
( q_1_2
| ~ p_2_2
| ~ q_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type12_1) ).
cnf(s2_type11_6,axiom,
( p_2_3
| ~ q_3_3
| ~ q_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type11_6) ).
cnf(s2_type11_5,axiom,
( p_2_3
| ~ p_3_3
| ~ p_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type11_5) ).
cnf(s2_type11_4,axiom,
( p_1_3
| ~ q_2_3
| ~ q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type11_4) ).
cnf(s2_type11_3,axiom,
( p_1_3
| ~ p_2_3
| ~ p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type11_3) ).
cnf(s2_type11_2,axiom,
( p_1_2
| ~ q_2_2
| ~ q_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type11_2) ).
cnf(sym_s2_type21_2,axiom,
( ~ sym_q_1_1
| sym_q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type21_2) ).
cnf(sym_s2_type21_1,axiom,
( ~ sym_p_1_1
| sym_p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sym_s2_type21_1) ).
cnf(s2_type22_4,axiom,
( q_3_3
| ~ q_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type22_4) ).
cnf(s2_type22_3,axiom,
( q_2_2
| ~ q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type22_3) ).
cnf(s2_type22_2,axiom,
( p_3_3
| ~ p_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type22_2) ).
cnf(s2_type11_1,axiom,
( p_1_2
| ~ p_2_2
| ~ p_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type11_1) ).
cnf(s2_type22_1,axiom,
( p_2_2
| ~ p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type22_1) ).
cnf(s2_type21_2,axiom,
( q_1_1
| ~ q_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type21_2) ).
cnf(s2_type21_1,axiom,
( p_1_1
| ~ p_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_type21_1) ).
cnf(s2_goal_1,negated_conjecture,
~ p_1_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_goal_1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN091-1.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 20:12:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.44/0.58 % Version: 1.5
% 0.44/0.58 % SZS status Satisfiable
% 0.44/0.58 % SZS output start Saturation
% See solution above
% 0.44/0.58
% 0.44/0.58 % Initial clauses : 38
% 0.44/0.58 % Processed clauses : 69
% 0.44/0.58 % Factors computed : 0
% 0.44/0.58 % Resolvents computed: 119
% 0.44/0.58 % Tautologies deleted: 0
% 0.44/0.58 % Forward subsumed : 88
% 0.44/0.58 % Backward subsumed : 10
% 0.44/0.58 % -------- CPU Time ---------
% 0.44/0.58 % User time : 0.233 s
% 0.44/0.58 % System time : 0.010 s
% 0.44/0.58 % Total time : 0.243 s
%------------------------------------------------------------------------------