%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN709-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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:49 EDT 2022
% Result : Unsatisfiable 22.17s 22.35s
% Output : Refutation 22.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 19
% Syntax : Number of clauses : 44 ( 14 unt; 0 nHn; 44 RR)
% Number of literals : 104 ( 0 equ; 64 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 13 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
p10(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(12,axiom,
p30(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(14,axiom,
p29(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(18,axiom,
p22(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(19,axiom,
p21(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(21,axiom,
p19(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(26,axiom,
p11(u,u),
file('SYN709-1.p',unknown),
[] ).
cnf(29,axiom,
p46(f23(c58,c56),f20(c59,c60)),
file('SYN709-1.p',unknown),
[] ).
cnf(44,axiom,
( ~ p30(u,v)
| ~ p30(u,w)
| p30(w,v) ),
file('SYN709-1.p',unknown),
[] ).
cnf(50,axiom,
( ~ p22(u,v)
| ~ p22(u,w)
| p22(w,v) ),
file('SYN709-1.p',unknown),
[] ).
cnf(53,axiom,
( ~ p19(u,v)
| ~ p19(u,w)
| p19(w,v) ),
file('SYN709-1.p',unknown),
[] ).
cnf(59,axiom,
p19(f25(f28(c64,u),f34(c66,v)),f34(u,v)),
file('SYN709-1.p',unknown),
[] ).
cnf(60,axiom,
( ~ p19(u,v)
| ~ p47(w,u)
| ~ p30(w,x)
| p47(x,v) ),
file('SYN709-1.p',unknown),
[] ).
cnf(63,axiom,
( ~ p11(u,v)
| ~ p46(w,u)
| ~ p22(w,x)
| p46(x,v) ),
file('SYN709-1.p',unknown),
[] ).
cnf(64,axiom,
~ p47(f31(f33(c62,c63),f34(c65,c56)),f25(f28(c64,c65),c60)),
file('SYN709-1.p',unknown),
[] ).
cnf(72,axiom,
( ~ p29(u,v)
| ~ p19(w,x)
| p30(f31(u,w),f31(v,x)) ),
file('SYN709-1.p',unknown),
[] ).
cnf(76,axiom,
( ~ p21(u,v)
| ~ p10(w,x)
| p22(f23(u,w),f23(v,x)) ),
file('SYN709-1.p',unknown),
[] ).
cnf(81,axiom,
( ~ p46(f23(c58,u),f20(c59,v))
| p47(f31(f33(c62,c63),f34(c66,u)),v) ),
file('SYN709-1.p',unknown),
[] ).
cnf(83,axiom,
( ~ p47(f31(f33(c62,c63),u),v)
| p47(f31(f33(c62,c63),f25(f28(c64,c65),u)),f25(f28(c64,c65),v)) ),
file('SYN709-1.p',unknown),
[] ).
cnf(108,plain,
( ~ p22(u,v)
| p22(v,u) ),
inference(res,[status(thm),theory(equality)],[18,50]),
[iquote('0:Res:18.0,50.0')] ).
cnf(114,plain,
( ~ p30(u,v)
| p30(v,u) ),
inference(res,[status(thm),theory(equality)],[12,44]),
[iquote('0:Res:12.0,44.0')] ).
cnf(133,plain,
( ~ p19(u,v)
| p19(v,u) ),
inference(res,[status(thm),theory(equality)],[21,53]),
[iquote('0:Res:21.0,53.0')] ).
cnf(136,plain,
p19(f34(u,v),f25(f28(c64,u),f34(c66,v))),
inference(res,[status(thm),theory(equality)],[59,133]),
[iquote('0:Res:59.0,133.0')] ).
cnf(153,plain,
( ~ p21(u,v)
| ~ p10(w,x)
| p22(f23(v,x),f23(u,w)) ),
inference(res,[status(thm),theory(equality)],[76,108]),
[iquote('0:Res:76.2,108.0')] ).
cnf(157,plain,
( ~ p29(u,v)
| ~ p19(w,x)
| p30(f31(v,x),f31(u,w)) ),
inference(res,[status(thm),theory(equality)],[72,114]),
[iquote('0:Res:72.2,114.0')] ).
cnf(180,plain,
( ~ p46(u,v)
| ~ p22(u,w)
| p46(w,v) ),
inference(res,[status(thm),theory(equality)],[26,63]),
[iquote('0:Res:26.0,63.0')] ).
cnf(183,plain,
( ~ p22(f23(c58,c56),u)
| p46(u,f20(c59,c60)) ),
inference(res,[status(thm),theory(equality)],[29,180]),
[iquote('0:Res:29.0,180.0')] ).
cnf(184,plain,
( ~ p22(f23(c58,c56),u)
| ~ p22(u,v)
| p46(v,f20(c59,c60)) ),
inference(res,[status(thm),theory(equality)],[183,180]),
[iquote('0:Res:183.1,180.0')] ).
cnf(195,plain,
( ~ p47(u,v)
| ~ p30(u,w)
| p47(w,v) ),
inference(res,[status(thm),theory(equality)],[21,60]),
[iquote('0:Res:21.0,60.0')] ).
cnf(209,plain,
( ~ p46(f23(c58,u),f20(c59,v))
| ~ p30(f31(f33(c62,c63),f34(c66,u)),w)
| p47(w,v) ),
inference(res,[status(thm),theory(equality)],[81,195]),
[iquote('0:Res:81.1,195.0')] ).
cnf(224,plain,
( ~ p21(u,c58)
| ~ p10(v,c56)
| ~ p22(f23(u,v),w)
| p46(w,f20(c59,c60)) ),
inference(res,[status(thm),theory(equality)],[153,184]),
[iquote('0:Res:153.2,184.0')] ).
cnf(225,plain,
( ~ p47(f31(f33(c62,c63),u),v)
| ~ p30(f31(f33(c62,c63),f25(f28(c64,c65),u)),w)
| p47(w,f25(f28(c64,c65),v)) ),
inference(res,[status(thm),theory(equality)],[83,195]),
[iquote('0:Res:83.1,195.0')] ).
cnf(295,plain,
( ~ p21(u,c58)
| ~ p10(v,c56)
| p46(f23(u,v),f20(c59,c60)) ),
inference(res,[status(thm),theory(equality)],[18,224]),
[iquote('0:Res:18.0,224.2')] ).
cnf(491,plain,
( ~ p29(u,f33(c62,c63))
| ~ p19(v,f34(c66,w))
| ~ p46(f23(c58,w),f20(c59,x))
| p47(f31(u,v),x) ),
inference(res,[status(thm),theory(equality)],[157,209]),
[iquote('0:Res:157.2,209.1')] ).
cnf(934,plain,
( ~ p29(u,f33(c62,c63))
| ~ p19(v,f25(f28(c64,c65),w))
| ~ p47(f31(f33(c62,c63),w),x)
| p47(f31(u,v),f25(f28(c64,c65),x)) ),
inference(res,[status(thm),theory(equality)],[157,225]),
[iquote('0:Res:157.2,225.1')] ).
cnf(3116,plain,
( ~ p21(c58,c58)
| ~ p10(u,c56)
| ~ p29(v,f33(c62,c63))
| ~ p19(w,f34(c66,u))
| p47(f31(v,w),c60) ),
inference(res,[status(thm),theory(equality)],[295,491]),
[iquote('0:Res:295.2,491.2')] ).
cnf(3122,plain,
( ~ p10(u,c56)
| ~ p29(v,f33(c62,c63))
| ~ p19(w,f34(c66,u))
| p47(f31(v,w),c60) ),
inference(mrr,[status(thm)],[3116,19]),
[iquote('0:MRR:3116.0,19.0')] ).
cnf(3286,plain,
( ~ p10(u,c56)
| ~ p19(v,f34(c66,u))
| p47(f31(f33(c62,c63),v),c60) ),
inference(res,[status(thm),theory(equality)],[14,3122]),
[iquote('0:Res:14.0,3122.1')] ).
cnf(3289,plain,
( ~ p10(u,c56)
| p47(f31(f33(c62,c63),f34(c66,u)),c60) ),
inference(res,[status(thm),theory(equality)],[21,3286]),
[iquote('0:Res:21.0,3286.1')] ).
cnf(3498,plain,
( ~ p29(u,f33(c62,c63))
| ~ p47(f31(f33(c62,c63),f34(c66,v)),w)
| p47(f31(u,f34(c65,v)),f25(f28(c64,c65),w)) ),
inference(res,[status(thm),theory(equality)],[136,934]),
[iquote('0:Res:136.0,934.1')] ).
cnf(19302,plain,
( ~ p29(f33(c62,c63),f33(c62,c63))
| ~ p47(f31(f33(c62,c63),f34(c66,c56)),c60) ),
inference(res,[status(thm),theory(equality)],[3498,64]),
[iquote('0:Res:3498.2,64.0')] ).
cnf(19310,plain,
~ p47(f31(f33(c62,c63),f34(c66,c56)),c60),
inference(mrr,[status(thm)],[19302,14]),
[iquote('0:MRR:19302.0,14.0')] ).
cnf(19315,plain,
~ p10(c56,c56),
inference(res,[status(thm),theory(equality)],[3289,19310]),
[iquote('0:Res:3289.1,19310.0')] ).
cnf(19325,plain,
$false,
inference(mrr,[status(thm)],[19315,1]),
[iquote('0:MRR:19315.0,1.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SYN709-1 : TPTP v8.1.0. Released v2.5.0.
% 0.07/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n017.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 : 600
% 0.12/0.33 % DateTime : Mon Jul 11 16:02:34 EDT 2022
% 0.12/0.33 % CPUTime :
% 22.17/22.35
% 22.17/22.35 SPASS V 3.9
% 22.17/22.35 SPASS beiseite: Proof found.
% 22.17/22.35 % SZS status Theorem
% 22.17/22.35 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.17/22.35 SPASS derived 19096 clauses, backtracked 0 clauses, performed 0 splits and kept 10312 clauses.
% 22.17/22.35 SPASS allocated 79642 KBytes.
% 22.17/22.35 SPASS spent 0:0:21.69 on the problem.
% 22.17/22.35 0:00:00.03 for the input.
% 22.17/22.35 0:00:00.00 for the FLOTTER CNF translation.
% 22.17/22.35 0:00:00.34 for inferences.
% 22.17/22.35 0:00:00.00 for the backtracking.
% 22.17/22.35 0:0:21.11 for the reduction.
% 22.17/22.35
% 22.17/22.35
% 22.17/22.35 Here is a proof with depth 9, length 44 :
% 22.17/22.35 % SZS output start Refutation
% See solution above
% 22.17/22.35 Formulae used in the proof : p10_1 p30_12 p29_14 p22_18 p21_19 p19_21 p11_26 p46_29 p30_44 p22_50 p19_53 p19_59 p47_60 p46_63 not_p47_64 p30_72 p22_76 p47_81 p47_83
% 22.17/22.35
%------------------------------------------------------------------------------