%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG211+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.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 : Fri Sep 25 12:52:05 PM UTC 2026
% Result : Theorem 3.45s 0.96s
% Output : Proof 3.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 52 ( 26 unt; 0 def)
% Number of atoms : 108 ( 23 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 92 ( 36 ~; 30 |; 18 &)
% ( 1 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-4 aty)
% Number of variables : 81 ( 4 sgn 41 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A,B] :
( a_vector_subspace_of(A,B)
=> a_vector_space(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bg_2_4_a) ).
fof(f3_nnf,plain,
! [A,B] :
( a_vector_space(A)
| ~ a_vector_subspace_of(A,B) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( a_vector_space(A)
| ~ a_vector_subspace_of(A,B) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c5,plain,
( a_vector_space(X0)
| ~ a_vector_subspace_of(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi5,axiom,
ifeq(a_vector_subspace_of(X0,X1),true,a_vector_space(X0),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
fof(f5,conjecture,
! [W,V] :
( ( a_vector_space(V)
& a_vector_subspace_of(W,V) )
=> ? [E,F] :
( basis_of(E,W)
& basis_of(union(E,F),V) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bg_2_4_3) ).
fof(f5_neg,negated_conjecture,
~ ! [W,V] :
( ( a_vector_space(V)
& a_vector_subspace_of(W,V) )
=> ? [E,F] :
( basis_of(E,W)
& basis_of(union(E,F),V) ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
? [W,V] :
( ! [E,F] :
( ~ basis_of(E,W)
| ~ basis_of(union(E,F),V) )
& a_vector_space(V)
& a_vector_subspace_of(W,V) ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
! [E,F] :
( ( ~ basis_of(E,sk2)
| ~ basis_of(union(E,F),sk3) )
& a_vector_space(sk3)
& a_vector_subspace_of(sk2,sk3) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3])],[f5_nnf]) ).
cnf(c8,plain,
a_vector_subspace_of(sk2,sk3),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi8,negated_conjecture,
a_vector_subspace_of(sk2,sk3) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h1,plain,
a_vector_space(sk2) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi8]) ).
fof(f2,axiom,
! [A] :
( a_vector_space(A)
=> ? [B] : basis_of(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bg_remark_63_a) ).
fof(f2_nnf,plain,
! [A] :
( ? [B] : basis_of(B,A)
| ~ a_vector_space(A) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] :
( basis_of(sk1(A),A)
| ~ a_vector_space(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f2_nnf]) ).
cnf(c4,plain,
( basis_of(sk1(X0),X0)
| ~ a_vector_space(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi4,axiom,
ifeq(a_vector_space(X0),true,basis_of(sk1(X0),X0),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h4,plain,
basis_of(sk1(sk2),sk2) = true,
inference(hyper_resolution,[status(thm)],[hi4,h1]) ).
cnf(c9,plain,
a_vector_space(sk3),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi9,negated_conjecture,
a_vector_space(sk3) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h0,plain,
basis_of(sk1(sk3),sk3) = true,
inference(hyper_resolution,[status(thm)],[hi4,hi9]) ).
fof(f0,axiom,
! [B,V] :
( basis_of(B,V)
=> ( a_subset_of(B,vec_to_class(V))
& lin_ind_subset(B,V) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',basis_of) ).
fof(f0_nnf,plain,
! [B,V] :
( ( a_subset_of(B,vec_to_class(V))
& lin_ind_subset(B,V) )
| ~ basis_of(B,V) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [B,V] :
( ( a_subset_of(B,vec_to_class(V))
& lin_ind_subset(B,V) )
| ~ basis_of(B,V) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( lin_ind_subset(X0,X1)
| ~ basis_of(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(basis_of(X0,X1),true,lin_ind_subset(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h3,plain,
lin_ind_subset(sk1(sk3),sk3) = true,
inference(hyper_resolution,[status(thm)],[hi0,h0]) ).
fof(f1,axiom,
! [S,T,V] :
( ( basis_of(T,V)
& lin_ind_subset(S,V) )
=> ? [U] :
( basis_of(union(S,U),V)
& a_subset_of(U,T) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bg_2_2_5) ).
fof(f1_nnf,plain,
! [S,T,V] :
( ? [U] :
( basis_of(union(S,U),V)
& a_subset_of(U,T) )
| ~ basis_of(T,V)
| ~ lin_ind_subset(S,V) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [S,V,T] :
( ( basis_of(union(S,sk0(S,T,V)),V)
& a_subset_of(sk0(S,T,V),T) )
| ~ basis_of(T,V)
| ~ lin_ind_subset(S,V) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f1_nnf]) ).
cnf(c3,plain,
( basis_of(union(X0,sk0(X0,X1,X2)),X2)
| ~ basis_of(X1,X2)
| ~ lin_ind_subset(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi3,axiom,
ifeq(lin_ind_subset(X0,X1),true,ifeq(basis_of(X2,X1),true,basis_of(union(X0,sk0(X0,X2,X1)),X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h5,plain,
basis_of(union(sk1(sk3),sk0(sk1(sk3),sk1(sk3),sk3)),sk3) = true,
inference(hyper_resolution,[status(thm)],[hi3,h3,h0]) ).
cnf(h9,plain,
basis_of(union(sk1(sk3),sk0(sk1(sk3),union(sk1(sk3),sk0(sk1(sk3),sk1(sk3),sk3)),sk3)),sk3) = true,
inference(hyper_resolution,[status(thm)],[hi3,h3,h5]) ).
cnf(h8,plain,
lin_ind_subset(sk1(sk2),sk2) = true,
inference(hyper_resolution,[status(thm)],[hi0,h4]) ).
cnf(c1,plain,
( a_subset_of(X0,vec_to_class(X1))
| ~ basis_of(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi1,axiom,
ifeq(basis_of(X0,X1),true,a_subset_of(X0,vec_to_class(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h7,plain,
a_subset_of(sk1(sk2),vec_to_class(sk2)) = true,
inference(hyper_resolution,[status(thm)],[hi1,h4]) ).
fof(f4,axiom,
! [W,V,E] :
( ( a_subset_of(E,vec_to_class(W))
& a_vector_subspace_of(W,V) )
=> ( lin_ind_subset(E,W)
<=> lin_ind_subset(E,V) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bg_2_4_2) ).
fof(f4_nnf,plain,
! [W,V,E] :
( ( ( ~ lin_ind_subset(E,V)
| lin_ind_subset(E,W) )
& ( lin_ind_subset(E,V)
| ~ lin_ind_subset(E,W) ) )
| ~ a_subset_of(E,vec_to_class(W))
| ~ a_vector_subspace_of(W,V) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [W,V,E] :
( ( ( ~ lin_ind_subset(E,V)
| lin_ind_subset(E,W) )
& ( lin_ind_subset(E,V)
| ~ lin_ind_subset(E,W) ) )
| ~ a_subset_of(E,vec_to_class(W))
| ~ a_vector_subspace_of(W,V) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c6,plain,
( lin_ind_subset(X2,X1)
| ~ lin_ind_subset(X2,X0)
| ~ a_subset_of(X2,vec_to_class(X0))
| ~ a_vector_subspace_of(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi6,axiom,
ifeq(a_vector_subspace_of(X0,X1),true,ifeq(a_subset_of(X2,vec_to_class(X0)),true,ifeq(lin_ind_subset(X2,X0),true,lin_ind_subset(X2,X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(h15,plain,
lin_ind_subset(sk1(sk2),sk3) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi8,h7,h8]) ).
cnf(h20,plain,
basis_of(union(sk1(sk2),sk0(sk1(sk2),union(sk1(sk3),sk0(sk1(sk3),union(sk1(sk3),sk0(sk1(sk3),sk1(sk3),sk3)),sk3)),sk3)),sk3) = true,
inference(hyper_resolution,[status(thm)],[hi3,h15,h9]) ).
cnf(c10,plain,
( ~ basis_of(X2,sk2)
| ~ basis_of(union(X2,X3),sk3) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi10,negated_conjecture,
ifeq(basis_of(union(X0,X1),sk3),true,ifeq(basis_of(X0,sk2),true,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi10,h20,h4]) ).
cnf(t319,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t319]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG211+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Fri Sep 25 05:04:35 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.45/0.96 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.45/0.96 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------