%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR147+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:05:02 AM UTC 2026
% Result : Theorem 10.03s 1.66s
% Output : CNFRefutation 10.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 26 ( 17 unt; 0 def)
% Number of atoms : 61 ( 2 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 68 ( 33 ~; 31 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-1 aty)
% Number of variables : 18 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(jim_human,axiom,
's$u$uHuman'(jim) ).
fof(experience,axiom,
! [X0,X1,X2] :
( 's$u$uHuman'(X0)
=> ( ( greater(X1,X2)
& 's$u$uage'('s$u$usiblingFn'(X0),X2)
& 's$u$uage'(X0,X1) )
=> ( 's$u$uhas$useen$umore'('s$u$usiblingFn'(X0),X0)
| 's$u$umore$uexperienced'(X0,'s$u$usiblingFn'(X0)) ) ) ) ).
fof(geoff_48,axiom,
's$u$uage'(geoff,n48) ).
fof(jim_54,axiom,
's$u$uage'(jim,n54) ).
fof(greater_54_48,axiom,
greater(n54,n48) ).
fof(geoff_and_jim,axiom,
geoff = 's$u$usiblingFn'(jim) ).
fof(jim_has_seen_more,axiom,
~ 's$u$uhas$useen$umore'(geoff,jim) ).
fof(jim_is_experienced,conjecture,
's$u$umore$uexperienced'(jim,geoff) ).
fof(negated_conjecture,negated_conjecture,
~ 's$u$umore$uexperienced'(jim,geoff),
inference(negate_conjecture,[status(cth)],[jim_is_experienced]) ).
cnf(c4,plain,
's$u$uHuman'(jim),
inference(clausification,[status(esa)],[jim_human]) ).
cnf(c6,plain,
( ~ 's$u$uage'(X0,X1)
| ~ 's$u$uHuman'(X0)
| ~ 's$u$uage'('s$u$usiblingFn'(X0),X2)
| 's$u$umore$uexperienced'(X0,'s$u$usiblingFn'(X0))
| ~ greater(X1,X2)
| 's$u$uhas$useen$umore'('s$u$usiblingFn'(X0),X0) ),
inference(clausification,[status(esa)],[experience]) ).
cnf(c8,plain,
's$u$uage'(geoff,n48),
inference(clausification,[status(esa)],[geoff_48]) ).
cnf(c9,plain,
's$u$uage'(jim,n54),
inference(clausification,[status(esa)],[jim_54]) ).
cnf(c10,plain,
greater(n54,n48),
inference(clausification,[status(esa)],[greater_54_48]) ).
cnf(c11,plain,
geoff = 's$u$usiblingFn'(jim),
inference(clausification,[status(esa)],[geoff_and_jim]) ).
cnf(c12,plain,
~ 's$u$uhas$useen$umore'(geoff,jim),
inference(clausification,[status(esa)],[jim_has_seen_more]) ).
cnf(c13,plain,
~ 's$u$umore$uexperienced'(jim,geoff),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( 's$u$umore$uexperienced'(jim,'s$u$usiblingFn'(jim))
| 's$u$uhas$useen$umore'('s$u$usiblingFn'(jim),jim)
| ~ greater(X1,X0)
| ~ 's$u$uage'(jim,X1)
| ~ 's$u$uHuman'(jim)
| ~ 's$u$uage'(geoff,X0) ),
inference(superposition,[status(thm)],[c11,c6]) ).
cnf(d1,plain,
( 's$u$umore$uexperienced'(jim,'s$u$usiblingFn'(jim))
| 's$u$uhas$useen$umore'(geoff,jim)
| ~ greater(X1,X0)
| ~ 's$u$uage'(jim,X1)
| ~ 's$u$uage'(geoff,X0)
| ~ 's$u$uHuman'(jim) ),
inference(demodulation,[status(thm)],[d0,c11]) ).
cnf(d2,plain,
( 's$u$umore$uexperienced'(jim,geoff)
| 's$u$uhas$useen$umore'(geoff,jim)
| ~ greater(X1,X0)
| ~ 's$u$uage'(jim,X1)
| ~ 's$u$uage'(geoff,X0)
| ~ 's$u$uHuman'(jim) ),
inference(demodulation,[status(thm)],[d1,c11]) ).
cnf(d3,plain,
( 's$u$uhas$useen$umore'(geoff,jim)
| ~ greater(X1,X0)
| ~ 's$u$uage'(jim,X1)
| ~ 's$u$uage'(geoff,X0)
| ~ 's$u$uHuman'(jim) ),
inference(resolution,[status(thm)],[c13,d2]) ).
cnf(d4,plain,
( 's$u$uhas$useen$umore'(geoff,jim)
| ~ greater(X1,X0)
| ~ 's$u$uage'(jim,X1)
| ~ 's$u$uage'(geoff,X0) ),
inference(resolution,[status(thm)],[c4,d3]) ).
cnf(d5,plain,
( ~ greater(X1,X0)
| ~ 's$u$uage'(jim,X1)
| ~ 's$u$uage'(geoff,X0) ),
inference(resolution,[status(thm)],[c12,d4]) ).
cnf(d6,plain,
( ~ 's$u$uage'(jim,n54)
| ~ 's$u$uage'(geoff,n48) ),
inference(resolution,[status(thm)],[d5,c10]) ).
cnf(d7,plain,
~ 's$u$uage'(jim,n54),
inference(resolution,[status(thm)],[c8,d6]) ).
cnf(d8,plain,
$false,
inference(resolution,[status(thm)],[c9,d7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR147+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 01:19:29 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.03/1.66 % SZS status Theorem for theBenchmark.p
% 10.03/1.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------