%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN704-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n010.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 : 600s
% DateTime : Thu Jul 21 12:23:47 EDT 2022
% Result : Unsatisfiable 1.48s 1.67s
% Output : Refutation 1.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 11
% Syntax : Number of clauses : 21 ( 9 unt; 0 nHn; 21 RR)
% Number of literals : 45 ( 0 equ; 25 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 17 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
p7(u,u),
file('SYN704-1.p',unknown),
[] ).
cnf(8,axiom,
p4(u,u),
file('SYN704-1.p',unknown),
[] ).
cnf(20,axiom,
p2(u,u),
file('SYN704-1.p',unknown),
[] ).
cnf(26,axiom,
p7(c54,c55),
file('SYN704-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ p7(u,v)
| ~ p7(u,w)
| p7(w,v) ),
file('SYN704-1.p',unknown),
[] ).
cnf(52,axiom,
~ p47(f20(f22(f24(f26(c56,u),v),w),x),x),
file('SYN704-1.p',unknown),
[] ).
cnf(53,axiom,
( ~ p4(u,v)
| ~ p7(w,x)
| ~ p47(u,w)
| p47(v,x) ),
file('SYN704-1.p',unknown),
[] ).
cnf(58,axiom,
( ~ p3(u,v)
| ~ p2(w,x)
| p4(f5(w,u),f5(x,v)) ),
file('SYN704-1.p',unknown),
[] ).
cnf(74,axiom,
( ~ p47(f5(c48,f13(f16(f18(c50,u),v),w)),x)
| p47(u,x) ),
file('SYN704-1.p',unknown),
[] ).
cnf(77,axiom,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55),
file('SYN704-1.p',unknown),
[] ).
cnf(80,axiom,
p3(f8(f10(c49,f13(f16(f18(c50,u),v),w)),x),f13(f16(f18(c50,f20(f22(f24(f26(c56,u),v),w),x)),f30(f32(f34(f36(c57,u),v),w),x)),f40(f42(f44(f46(c58,u),v),w),x))),
file('SYN704-1.p',unknown),
[] ).
cnf(130,plain,
( ~ p7(u,v)
| p7(v,u) ),
inference(res,[status(thm),theory(equality)],[3,29]),
[iquote('0:Res:3.0,29.0')] ).
cnf(133,plain,
p7(c55,c54),
inference(res,[status(thm),theory(equality)],[26,130]),
[iquote('0:Res:26.0,130.0')] ).
cnf(180,plain,
( ~ p7(u,v)
| ~ p47(w,u)
| p47(w,v) ),
inference(res,[status(thm),theory(equality)],[8,53]),
[iquote('0:Res:8.0,53.0')] ).
cnf(181,plain,
( ~ p3(u,v)
| ~ p2(w,x)
| ~ p7(y,z)
| ~ p47(f5(w,u),y)
| p47(f5(x,v),z) ),
inference(res,[status(thm),theory(equality)],[58,53]),
[iquote('0:Res:58.2,53.0')] ).
cnf(185,plain,
( ~ p47(u,c55)
| p47(u,c54) ),
inference(res,[status(thm),theory(equality)],[133,180]),
[iquote('0:Res:133.0,180.0')] ).
cnf(188,plain,
( ~ p47(f5(c48,f13(f16(f18(c50,u),v),w)),c55)
| p47(u,c54) ),
inference(res,[status(thm),theory(equality)],[185,74]),
[iquote('0:Res:185.1,74.0')] ).
cnf(330,plain,
( ~ p3(f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54),u)
| ~ p2(c48,v)
| ~ p7(c55,w)
| p47(f5(v,u),w) ),
inference(res,[status(thm),theory(equality)],[77,181]),
[iquote('0:Res:77.0,181.3')] ).
cnf(772,plain,
( ~ p2(c48,u)
| ~ p7(c55,v)
| p47(f5(u,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))),v) ),
inference(res,[status(thm),theory(equality)],[80,330]),
[iquote('0:Res:80.0,330.0')] ).
cnf(4578,plain,
( ~ p2(c48,c48)
| ~ p7(c55,c55)
| p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c54) ),
inference(res,[status(thm),theory(equality)],[772,188]),
[iquote('0:Res:772.2,188.0')] ).
cnf(4586,plain,
$false,
inference(mrr,[status(thm)],[4578,20,3,52]),
[iquote('0:MRR:4578.0,4578.1,4578.2,20.0,3.0,52.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN704-1 : TPTP v8.1.0. Released v2.5.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n010.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 : 600
% 0.13/0.34 % DateTime : Mon Jul 11 14:47:45 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.48/1.67
% 1.48/1.67 SPASS V 3.9
% 1.48/1.67 SPASS beiseite: Proof found.
% 1.48/1.67 % SZS status Theorem
% 1.48/1.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.48/1.67 SPASS derived 4460 clauses, backtracked 0 clauses, performed 0 splits and kept 2296 clauses.
% 1.48/1.67 SPASS allocated 67711 KBytes.
% 1.48/1.67 SPASS spent 0:00:01.30 on the problem.
% 1.48/1.67 0:00:00.04 for the input.
% 1.48/1.67 0:00:00.00 for the FLOTTER CNF translation.
% 1.48/1.67 0:00:00.07 for inferences.
% 1.48/1.67 0:00:00.00 for the backtracking.
% 1.48/1.67 0:00:01.11 for the reduction.
% 1.48/1.67
% 1.48/1.67
% 1.48/1.67 Here is a proof with depth 5, length 21 :
% 1.48/1.67 % SZS output start Refutation
% See solution above
% 1.48/1.67 Formulae used in the proof : p7_3 p4_8 p2_20 p7_26 p7_29 not_p47_52 p47_53 p4_58 p47_74 p47_77 p3_80
% 1.48/1.67
%------------------------------------------------------------------------------