%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW364+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 09:11:45 AM UTC 2026
% Result : Theorem 179.90s 26.10s
% Output : CNFRefutation 179.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of formulae : 51 ( 32 unt; 0 def)
% Number of atoms : 71 ( 17 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 37 ( 17 ~; 13 |; 0 &)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 80 ( 12 sgn 31 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_assms_I1_J,axiom,
! [X0,X1] :
( hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'('t$ua','tc$uHOL$uObool')),X1),X0))
=> 'v$uP'(X0,X1) ) ).
fof(fact_empty__subsetI,axiom,
! [X0,X1] : hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X1,'tc$uHOL$uObool')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool'))),X0)) ).
fof(fact_emptyE,axiom,
! [X0,X1] : ~ hBOOL(hAPP(hAPP('c$umember'(X1),X0),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool')))) ).
fof(fact_insert__code,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(hAPP('c$uSet$uOinsert'(X3),X2),X1),X0))
<=> ( hBOOL(hAPP(X1,X0))
| X2 = X0 ) ) ).
fof(fact_insert__commute,axiom,
! [X0,X1,X2,X3] : hAPP(hAPP('c$uSet$uOinsert'(X3),X2),hAPP(hAPP('c$uSet$uOinsert'(X3),X1),X0)) = hAPP(hAPP('c$uSet$uOinsert'(X3),X1),hAPP(hAPP('c$uSet$uOinsert'(X3),X2),X0)) ).
fof(fact_ex__in__conv,axiom,
! [X0,X1] :
( ? [X2] : hBOOL(hAPP(hAPP('c$umember'(X1),X2),X0))
<=> X0 != 'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool')) ) ).
fof(fact_all__not__in__conv,axiom,
! [X0,X1] :
( ! [X2] : ~ hBOOL(hAPP(hAPP('c$umember'(X1),X2),X0))
<=> X0 = 'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool')) ) ).
fof(fact_insert__absorb,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP('c$umember'(X2),X1),X0))
=> hAPP(hAPP('c$uSet$uOinsert'(X2),X1),X0) = X0 ) ).
fof(fact_insert__mono,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X3,'tc$uHOL$uObool')),X2),X1))
=> hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X3,'tc$uHOL$uObool')),hAPP(hAPP('c$uSet$uOinsert'(X3),X0),X2)),hAPP(hAPP('c$uSet$uOinsert'(X3),X0),X1))) ) ).
fof(fact_subset__insertI,axiom,
! [X0,X1,X2] : hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X2,'tc$uHOL$uObool')),X1),hAPP(hAPP('c$uSet$uOinsert'(X2),X0),X1))) ).
fof(fact_bot__empty__eq,axiom,
! [X0,X1] :
( hBOOL(hAPP('c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool')),X0))
<=> hBOOL(hAPP(hAPP('c$umember'(X1),X0),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X1,'tc$uHOL$uObool')))) ) ).
fof(conj_6,hypothesis,
hBOOL(hAPP(hAPP('c$umember'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'v$uG')) ).
fof(conj_7,conjecture,
'v$uP'('v$uG',hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('t$ua','tc$uHOL$uObool')))) ).
fof(negated_conjecture,negated_conjecture,
~ 'v$uP'('v$uG',hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('t$ua','tc$uHOL$uObool')))),
inference(negate_conjecture,[status(cth)],[conj_7]) ).
cnf(c1,plain,
( 'v$uP'(X1,X0)
| ~ hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'('t$ua','tc$uHOL$uObool')),X0),X1)) ),
inference(clausification,[status(esa)],[fact_assms_I1_J]) ).
cnf(c2,plain,
hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool'))),X1)),
inference(clausification,[status(esa)],[fact_empty__subsetI]) ).
cnf(c8,plain,
~ hBOOL(hAPP(hAPP('c$umember'(X0),X1),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool')))),
inference(clausification,[status(esa)],[fact_emptyE]) ).
cnf(c10,plain,
( X3 != X1
| hBOOL(hAPP(hAPP(hAPP('c$uSet$uOinsert'(X0),X1),X2),X3)) ),
inference(clausification,[status(esa)],[fact_insert__code]) ).
cnf(c12,plain,
hAPP(hAPP('c$uSet$uOinsert'(X0),X1),hAPP(hAPP('c$uSet$uOinsert'(X0),X2),X3)) = hAPP(hAPP('c$uSet$uOinsert'(X0),X2),hAPP(hAPP('c$uSet$uOinsert'(X0),X1),X3)),
inference(clausification,[status(esa)],[fact_insert__commute]) ).
cnf(c17,plain,
( 'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool')) = X1
| hBOOL(hAPP(hAPP('c$umember'(X0),sK40(X1,X0)),X1)) ),
inference(clausification,[status(esa)],[fact_ex__in__conv]) ).
cnf(c18,plain,
( 'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool')) = X1
| hBOOL(hAPP(hAPP('c$umember'(X0),sK43(X1,X0)),X1)) ),
inference(clausification,[status(esa)],[fact_all__not__in__conv]) ).
cnf(c20,plain,
( hAPP(hAPP('c$uSet$uOinsert'(X0),X1),X2) = X2
| ~ hBOOL(hAPP(hAPP('c$umember'(X0),X1),X2)) ),
inference(clausification,[status(esa)],[fact_insert__absorb]) ).
cnf(c42,plain,
( hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool')),hAPP(hAPP('c$uSet$uOinsert'(X0),X3),X1)),hAPP(hAPP('c$uSet$uOinsert'(X0),X3),X2)))
| ~ hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool')),X1),X2)) ),
inference(clausification,[status(esa)],[fact_insert__mono]) ).
cnf(c44,plain,
hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool')),X1),hAPP(hAPP('c$uSet$uOinsert'(X0),X2),X1))),
inference(clausification,[status(esa)],[fact_subset__insertI]) ).
cnf(c56,plain,
( hBOOL(hAPP(hAPP('c$umember'(X0),X1),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool'))))
| ~ hBOOL(hAPP('c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool')),X1)) ),
inference(clausification,[status(esa)],[fact_bot__empty__eq]) ).
cnf(c125,plain,
hBOOL(hAPP(hAPP('c$umember'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'v$uG')),
inference(clausification,[status(esa)],[conj_6]) ).
cnf(c126,plain,
~ 'v$uP'('v$uG',hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('t$ua','tc$uHOL$uObool')))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'(X0,'tc$uHOL$uObool')),hAPP(hAPP('c$uSet$uOinsert'(X0),X1),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool')))),hAPP(hAPP('c$uSet$uOinsert'(X0),X1),X2))),
inference(resolution,[status(thm)],[c42,c2]) ).
cnf(d1,plain,
hBOOL(hAPP(hAPP(hAPP('c$uSet$uOinsert'(X0),X1),X2),X1)),
inference(equality_resolution,[status(thm)],[c10]) ).
cnf(d2,plain,
( hBOOL(hAPP(hAPP('c$umember'('t$ua'),sK43(X0,'t$ua')),X0))
| ~ 'v$uP'('v$uG',hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),X0)) ),
inference(superposition,[status(thm)],[c18,c126]) ).
cnf(d3,plain,
hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'v$uG') = 'v$uG',
inference(resolution,[status(thm)],[c20,c125]) ).
cnf(d4,plain,
( hBOOL(hAPP(hAPP('c$umember'('t$ua'),sK43('v$uG','t$ua')),'v$uG'))
| ~ 'v$uP'('v$uG','v$uG') ),
inference(superposition,[status(thm)],[d3,d2]) ).
cnf(d5,plain,
'v$uP'(hAPP(hAPP('c$uSet$uOinsert'('t$ua'),X0),X1),X1),
inference(resolution,[status(thm)],[c44,c1]) ).
cnf(d6,plain,
'v$uP'('v$uG','v$uG'),
inference(superposition,[status(thm)],[d3,d5]) ).
cnf(d7,plain,
hBOOL(hAPP(hAPP('c$umember'('t$ua'),sK43('v$uG','t$ua')),'v$uG')),
inference(resolution,[status(thm)],[d6,d4]) ).
cnf(d8,plain,
hAPP(hAPP('c$uSet$uOinsert'('t$ua'),sK43('v$uG','t$ua')),'v$uG') = 'v$uG',
inference(resolution,[status(thm)],[d7,c20]) ).
cnf(d9,plain,
hBOOL(hAPP('v$uG',sK43('v$uG','t$ua'))),
inference(superposition,[status(thm)],[d8,d1]) ).
cnf(d10,plain,
~ hBOOL(hAPP('c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'(X0,'tc$uHOL$uObool')),X1)),
inference(resolution,[status(thm)],[c8,c56]) ).
cnf(d11,plain,
( hBOOL(hAPP(hAPP('c$umember'(X0),sK40(X1,X0)),X1))
| ~ hBOOL(hAPP(X1,X2)) ),
inference(superposition,[status(thm)],[c17,d10]) ).
cnf(d12,plain,
hBOOL(hAPP(hAPP('c$umember'(X0),sK40('v$uG',X0)),'v$uG')),
inference(resolution,[status(thm)],[d11,d9]) ).
cnf(d13,plain,
hAPP(hAPP('c$uSet$uOinsert'(X0),sK40('v$uG',X0)),'v$uG') = 'v$uG',
inference(resolution,[status(thm)],[d12,c20]) ).
cnf(d14,plain,
( hBOOL(hAPP(hAPP('c$umember'('t$ua'),sK40(X0,'t$ua')),X0))
| ~ 'v$uP'('v$uG',hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),X0)) ),
inference(superposition,[status(thm)],[c17,c126]) ).
cnf(d15,plain,
( hBOOL(hAPP(hAPP('c$umember'('t$ua'),sK40('v$uG','t$ua')),'v$uG'))
| ~ 'v$uP'('v$uG','v$uG') ),
inference(superposition,[status(thm)],[d3,d14]) ).
cnf(d16,plain,
hBOOL(hAPP(hAPP('c$umember'('t$ua'),sK40('v$uG','t$ua')),'v$uG')),
inference(resolution,[status(thm)],[d6,d15]) ).
cnf(d17,plain,
hAPP(hAPP('c$uSet$uOinsert'('t$ua'),sK40('v$uG','t$ua')),'v$uG') = 'v$uG',
inference(resolution,[status(thm)],[d16,c20]) ).
cnf(d18,plain,
hAPP(hAPP('c$uSet$uOinsert'('t$ua'),sK40('v$uG','t$ua')),hAPP(hAPP('c$uSet$uOinsert'('t$ua'),X0),'v$uG')) = hAPP(hAPP('c$uSet$uOinsert'('t$ua'),X0),'v$uG'),
inference(superposition,[status(thm)],[d17,c12]) ).
cnf(d19,plain,
hAPP(hAPP('c$uSet$uOinsert'('t$ua'),sK40('v$uG','t$ua')),'v$uG') = hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'v$uG'),
inference(superposition,[status(thm)],[d3,d18]) ).
cnf(d20,plain,
'v$uG' = hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'v$uG'),
inference(demodulation,[status(thm)],[d19,d13]) ).
cnf(d21,plain,
hBOOL(hAPP(hAPP('c$uOrderings$uOord$u$uclass$uOless$u$ueq'('tc$ufun'('t$ua','tc$uHOL$uObool')),hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('t$ua','tc$uHOL$uObool')))),'v$uG')),
inference(superposition,[status(thm)],[d20,d0]) ).
cnf(d22,plain,
'v$uP'('v$uG',hAPP(hAPP('c$uSet$uOinsert'('t$ua'),hAPP('v$umgt$u$ucall','v$upn')),'c$uOrderings$uObot$u$uclass$uObot'('tc$ufun'('t$ua','tc$uHOL$uObool')))),
inference(resolution,[status(thm)],[d21,c1]) ).
cnf(d23,plain,
$false,
inference(resolution,[status(thm)],[c126,d22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW364+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 15:48:29 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 179.90/26.10 % SZS status Theorem for theBenchmark.p
% 179.90/26.10 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------