%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PLA007-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 : Tue Sep 29 12:27:41 PM UTC 2026
% Result : Unsatisfiable 15.22s 3.38s
% Output : Refutation 16.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 35
% Syntax : Number of formulae : 157 ( 69 unt; 16 def)
% Number of atoms : 303 ( 115 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 283 ( 137 ~; 131 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 16 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-4 aty)
% Number of variables : 73 ( 0 sgn 73 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f4,axiom,
! [X0,X1] : ifeq(differ(X0,table),true,ifeq(holds(empty,X1),true,ifeq(holds(clear(X0),X1),true,holds(holding(X0),do(pickup(X0),X1)),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pickup_1) ).
fof(f5,plain,
! [X0,X1] : true = ifeq(differ(X0,table),true,ifeq(holds(empty,X1),true,ifeq(holds(clear(X0),X1),true,holds(holding(X0),do(pickup(X0),X1)),true),true),true),
inference(reorient_equations,[],[f4]) ).
fof(f6,axiom,
! [X2,X0,X1] : ifeq(holds(on(X0,X1),X2),true,ifeq(holds(empty,X2),true,ifeq(holds(clear(X0),X2),true,holds(clear(X1),do(pickup(X0),X2)),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pickup_2) ).
fof(f7,plain,
! [X2,X0,X1] : true = ifeq(holds(on(X0,X1),X2),true,ifeq(holds(empty,X2),true,ifeq(holds(clear(X0),X2),true,holds(clear(X1),do(pickup(X0),X2)),true),true),true),
inference(reorient_equations,[],[f6]) ).
fof(f10,axiom,
! [X2,X0,X1] : ifeq(differ(X0,X1),true,ifeq(holds(clear(X0),X2),true,holds(clear(X0),do(pickup(X1),X2)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pickup_4) ).
fof(f11,plain,
! [X2,X0,X1] : true = ifeq(differ(X0,X1),true,ifeq(holds(clear(X0),X2),true,holds(clear(X0),do(pickup(X1),X2)),true),true),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
! [X2,X0,X1] : ifeq(holds(holding(X0),X1),true,ifeq(holds(clear(X2),X1),true,holds(empty,do(putdown(X0,X2),X1)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',putdown_1) ).
fof(f13,plain,
! [X2,X0,X1] : true = ifeq(holds(holding(X0),X1),true,ifeq(holds(clear(X2),X1),true,holds(empty,do(putdown(X0,X2),X1)),true),true),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X2,X0,X1] : ifeq(holds(holding(X0),X1),true,ifeq(holds(clear(X2),X1),true,holds(on(X0,X2),do(putdown(X0,X2),X1)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',putdown_2) ).
fof(f15,plain,
! [X2,X0,X1] : true = ifeq(holds(holding(X0),X1),true,ifeq(holds(clear(X2),X1),true,holds(on(X0,X2),do(putdown(X0,X2),X1)),true),true),
inference(reorient_equations,[],[f14]) ).
fof(f20,axiom,
! [X2,X3,X0,X1] : ifeq(differ(X0,X1),true,ifeq(holds(clear(X0),X2),true,holds(clear(X0),do(putdown(X3,X1),X2)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',putdown_5) ).
fof(f21,plain,
! [X2,X3,X0,X1] : true = ifeq(differ(X0,X1),true,ifeq(holds(clear(X0),X2),true,holds(clear(X0),do(putdown(X3,X1),X2)),true),true),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0,X1] : ifeq(differ(X0,X1),true,differ(X1,X0),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_differ) ).
fof(f23,plain,
! [X0,X1] : true = ifeq(differ(X0,X1),true,differ(X1,X0),true),
inference(reorient_equations,[],[f22]) ).
fof(f26,axiom,
differ(a,c) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',differ_a_c) ).
fof(f27,plain,
true = differ(a,c),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
differ(a,d) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',differ_a_d) ).
fof(f29,plain,
true = differ(a,d),
inference(reorient_equations,[],[f28]) ).
fof(f30,axiom,
differ(a,table) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',differ_a_table) ).
fof(f31,plain,
true = differ(a,table),
inference(reorient_equations,[],[f30]) ).
fof(f40,axiom,
differ(c,table) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',differ_c_table) ).
fof(f41,plain,
true = differ(c,table),
inference(reorient_equations,[],[f40]) ).
fof(f42,axiom,
differ(d,table) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',differ_d_table) ).
fof(f43,plain,
true = differ(d,table),
inference(reorient_equations,[],[f42]) ).
fof(f48,axiom,
holds(on(c,d),s0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',initial_state3) ).
fof(f49,plain,
true = holds(on(c,d),s0),
inference(reorient_equations,[],[f48]) ).
fof(f52,axiom,
holds(clear(a),s0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',initial_state5) ).
fof(f53,plain,
true = holds(clear(a),s0),
inference(reorient_equations,[],[f52]) ).
fof(f56,axiom,
holds(clear(c),s0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',initial_state7) ).
fof(f57,plain,
true = holds(clear(c),s0),
inference(reorient_equations,[],[f56]) ).
fof(f58,axiom,
holds(empty,s0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',initial_state8) ).
fof(f59,plain,
true = holds(empty,s0),
inference(reorient_equations,[],[f58]) ).
fof(f60,axiom,
! [X0] : holds(clear(table),X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clear_table) ).
fof(f61,plain,
! [X0] : true = holds(clear(table),X0),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
! [X0] : holds(on(a,d),X0) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_AD) ).
fof(f63,plain,
! [X0] : true != holds(on(a,d),X0),
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF0 = on(a,d),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f65,plain,
on(a,d) = sF0,
inference(reorient_equations,[],[f64]) ).
fof(f66,plain,
! [X0] : true != holds(sF0,X0),
inference(definition_folding,[],[f63,f65]) ).
fof(f68,definition,
( spl1_1
<=> on(a,d) = sF0 ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f70,plain,
( on(a,d) = sF0
| ~ spl1_1 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f71,plain,
spl1_1,
inference(avatar_split_clause,[],[f65,f68]) ).
fof(f73,plain,
( ! [X0] : true = ifeq(holds(holding(a),X0),true,ifeq(holds(clear(d),X0),true,holds(sF0,do(putdown(a,d),X0)),true),true)
| ~ spl1_1 ),
inference(superposition,[],[f15,f70]) ).
fof(f82,definition,
( spl1_3
<=> true = differ(a,c) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f84,plain,
( true = differ(a,c)
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f85,plain,
spl1_3,
inference(avatar_split_clause,[],[f27,f82]) ).
fof(f87,definition,
( spl1_4
<=> true = differ(a,d) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f89,plain,
( true = differ(a,d)
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f90,plain,
spl1_4,
inference(avatar_split_clause,[],[f29,f87]) ).
fof(f121,definition,
( spl1_7
<=> true = holds(empty,s0) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f123,plain,
( true = holds(empty,s0)
| ~ spl1_7 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,plain,
spl1_7,
inference(avatar_split_clause,[],[f59,f121]) ).
fof(f133,definition,
( spl1_8
<=> true = differ(a,table) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f135,plain,
( true = differ(a,table)
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f133]) ).
fof(f136,plain,
spl1_8,
inference(avatar_split_clause,[],[f31,f133]) ).
fof(f145,plain,
! [X0,X1] : true = ifeq(holds(holding(X0),X1),true,ifeq(true,true,holds(empty,do(putdown(X0,table),X1)),true),true),
inference(superposition,[],[f13,f61]) ).
fof(f146,plain,
! [X0,X1] : true = ifeq(holds(holding(X0),X1),true,holds(empty,do(putdown(X0,table),X1)),true),
inference(forward_demodulation,[],[f145,f1]) ).
fof(f148,definition,
( spl1_9
<=> true = differ(d,table) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f150,plain,
( true = differ(d,table)
| ~ spl1_9 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,plain,
spl1_9,
inference(avatar_split_clause,[],[f43,f148]) ).
fof(f153,definition,
( spl1_10
<=> true = holds(clear(a),s0) ),
introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition]) ).
fof(f155,plain,
( true = holds(clear(a),s0)
| ~ spl1_10 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,plain,
spl1_10,
inference(avatar_split_clause,[],[f53,f153]) ).
fof(f207,plain,
( ! [X0] : true = ifeq(true,true,ifeq(holds(clear(a),X0),true,holds(clear(a),do(pickup(c),X0)),true),true)
| ~ spl1_3 ),
inference(superposition,[],[f11,f84]) ).
fof(f210,plain,
( ! [X0] : true = ifeq(holds(clear(a),X0),true,holds(clear(a),do(pickup(c),X0)),true)
| ~ spl1_3 ),
inference(forward_demodulation,[],[f207,f1]) ).
fof(f214,plain,
( true = ifeq(true,true,holds(clear(a),do(pickup(c),s0)),true)
| ~ spl1_3
| ~ spl1_10 ),
inference(superposition,[],[f210,f155]) ).
fof(f217,plain,
( true = holds(clear(a),do(pickup(c),s0))
| ~ spl1_3
| ~ spl1_10 ),
inference(forward_demodulation,[],[f214,f1]) ).
fof(f223,plain,
( true = ifeq(true,true,differ(d,a),true)
| ~ spl1_4 ),
inference(superposition,[],[f23,f89]) ).
fof(f230,plain,
( true = differ(d,a)
| ~ spl1_4 ),
inference(forward_demodulation,[],[f223,f1]) ).
fof(f290,definition,
( spl1_13
<=> true = holds(clear(c),s0) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
fof(f292,plain,
( true = holds(clear(c),s0)
| ~ spl1_13 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,plain,
spl1_13,
inference(avatar_split_clause,[],[f57,f290]) ).
fof(f296,plain,
( true = ifeq(differ(c,table),true,ifeq(holds(empty,s0),true,ifeq(true,true,holds(holding(c),do(pickup(c),s0)),true),true),true)
| ~ spl1_13 ),
inference(superposition,[],[f5,f292]) ).
fof(f313,plain,
( true = ifeq(differ(c,table),true,ifeq(holds(empty,s0),true,holds(holding(c),do(pickup(c),s0)),true),true)
| ~ spl1_13 ),
inference(forward_demodulation,[],[f296,f1]) ).
fof(f317,plain,
( true = ifeq(differ(c,table),true,ifeq(true,true,holds(holding(c),do(pickup(c),s0)),true),true)
| ~ spl1_7
| ~ spl1_13 ),
inference(forward_demodulation,[],[f313,f123]) ).
fof(f319,plain,
( true = ifeq(differ(c,table),true,holds(holding(c),do(pickup(c),s0)),true)
| ~ spl1_7
| ~ spl1_13 ),
inference(forward_demodulation,[],[f317,f1]) ).
fof(f320,plain,
( true = ifeq(true,true,holds(holding(c),do(pickup(c),s0)),true)
| ~ spl1_7
| ~ spl1_13 ),
inference(forward_demodulation,[],[f319,f41]) ).
fof(f321,plain,
( true = holds(holding(c),do(pickup(c),s0))
| ~ spl1_7
| ~ spl1_13 ),
inference(forward_demodulation,[],[f320,f1]) ).
fof(f323,definition,
( spl1_14
<=> true = holds(holding(c),do(pickup(c),s0)) ),
introduced(definition,[new_symbols(definition,[spl1_14])],[avatar_definition]) ).
fof(f325,plain,
( true = holds(holding(c),do(pickup(c),s0))
| ~ spl1_14 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f326,plain,
( spl1_14
| ~ spl1_7
| ~ spl1_13 ),
inference(avatar_split_clause,[],[f321,f290,f121,f323]) ).
fof(f410,plain,
( ! [X0,X1] : true = ifeq(true,true,ifeq(holds(clear(d),X0),true,holds(clear(d),do(putdown(X1,table),X0)),true),true)
| ~ spl1_9 ),
inference(superposition,[],[f21,f150]) ).
fof(f415,plain,
( ! [X0,X1] : true = ifeq(holds(clear(d),X0),true,holds(clear(d),do(putdown(X1,table),X0)),true)
| ~ spl1_9 ),
inference(forward_demodulation,[],[f410,f1]) ).
fof(f422,plain,
( ! [X0] : true = ifeq(true,true,ifeq(holds(empty,X0),true,ifeq(holds(clear(a),X0),true,holds(holding(a),do(pickup(a),X0)),true),true),true)
| ~ spl1_8 ),
inference(superposition,[],[f5,f135]) ).
fof(f425,plain,
( ! [X0,X1] : true = ifeq(true,true,ifeq(holds(clear(a),X0),true,holds(clear(a),do(putdown(X1,table),X0)),true),true)
| ~ spl1_8 ),
inference(superposition,[],[f21,f135]) ).
fof(f430,plain,
( ! [X0,X1] : true = ifeq(holds(clear(a),X0),true,holds(clear(a),do(putdown(X1,table),X0)),true)
| ~ spl1_8 ),
inference(forward_demodulation,[],[f425,f1]) ).
fof(f432,plain,
( ! [X0] : true = ifeq(holds(empty,X0),true,ifeq(holds(clear(a),X0),true,holds(holding(a),do(pickup(a),X0)),true),true)
| ~ spl1_8 ),
inference(forward_demodulation,[],[f422,f1]) ).
fof(f460,definition,
( spl1_19
<=> true = holds(on(c,d),s0) ),
introduced(definition,[new_symbols(definition,[spl1_19])],[avatar_definition]) ).
fof(f462,plain,
( true = holds(on(c,d),s0)
| ~ spl1_19 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f463,plain,
spl1_19,
inference(avatar_split_clause,[],[f49,f460]) ).
fof(f465,plain,
( true = ifeq(true,true,ifeq(holds(empty,s0),true,ifeq(holds(clear(c),s0),true,holds(clear(d),do(pickup(c),s0)),true),true),true)
| ~ spl1_19 ),
inference(superposition,[],[f7,f462]) ).
fof(f472,plain,
( true = ifeq(holds(empty,s0),true,ifeq(holds(clear(c),s0),true,holds(clear(d),do(pickup(c),s0)),true),true)
| ~ spl1_19 ),
inference(forward_demodulation,[],[f465,f1]) ).
fof(f474,plain,
( true = ifeq(holds(empty,s0),true,ifeq(true,true,holds(clear(d),do(pickup(c),s0)),true),true)
| ~ spl1_13
| ~ spl1_19 ),
inference(forward_demodulation,[],[f472,f292]) ).
fof(f475,plain,
( true = ifeq(holds(empty,s0),true,holds(clear(d),do(pickup(c),s0)),true)
| ~ spl1_13
| ~ spl1_19 ),
inference(forward_demodulation,[],[f474,f1]) ).
fof(f476,plain,
( true = ifeq(true,true,holds(clear(d),do(pickup(c),s0)),true)
| ~ spl1_7
| ~ spl1_13
| ~ spl1_19 ),
inference(forward_demodulation,[],[f475,f123]) ).
fof(f477,plain,
( true = holds(clear(d),do(pickup(c),s0))
| ~ spl1_7
| ~ spl1_13
| ~ spl1_19 ),
inference(forward_demodulation,[],[f476,f1]) ).
fof(f479,definition,
( spl1_20
<=> true = holds(clear(d),do(pickup(c),s0)) ),
introduced(definition,[new_symbols(definition,[spl1_20])],[avatar_definition]) ).
fof(f481,plain,
( true = holds(clear(d),do(pickup(c),s0))
| ~ spl1_20 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,plain,
( spl1_20
| ~ spl1_7
| ~ spl1_13
| ~ spl1_19 ),
inference(avatar_split_clause,[],[f477,f460,f290,f121,f479]) ).
fof(f483,plain,
( ! [X0] : true = ifeq(true,true,holds(clear(d),do(putdown(X0,table),do(pickup(c),s0))),true)
| ~ spl1_9
| ~ spl1_20 ),
inference(superposition,[],[f415,f481]) ).
fof(f508,plain,
( ! [X0] : true = holds(clear(d),do(putdown(X0,table),do(pickup(c),s0)))
| ~ spl1_9
| ~ spl1_20 ),
inference(forward_demodulation,[],[f483,f1]) ).
fof(f666,plain,
( true = ifeq(true,true,holds(empty,do(putdown(c,table),do(pickup(c),s0))),true)
| ~ spl1_14 ),
inference(superposition,[],[f146,f325]) ).
fof(f669,plain,
( true = holds(empty,do(putdown(c,table),do(pickup(c),s0)))
| ~ spl1_14 ),
inference(forward_demodulation,[],[f666,f1]) ).
fof(f767,definition,
( spl1_26
<=> true = holds(empty,do(putdown(c,table),do(pickup(c),s0))) ),
introduced(definition,[new_symbols(definition,[spl1_26])],[avatar_definition]) ).
fof(f769,plain,
( true = holds(empty,do(putdown(c,table),do(pickup(c),s0)))
| ~ spl1_26 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f770,plain,
( spl1_26
| ~ spl1_14 ),
inference(avatar_split_clause,[],[f669,f323,f767]) ).
fof(f1124,definition,
( spl1_41
<=> true = differ(d,a) ),
introduced(definition,[new_symbols(definition,[spl1_41])],[avatar_definition]) ).
fof(f1126,plain,
( true = differ(d,a)
| ~ spl1_41 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1127,plain,
( spl1_41
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f230,f87,f1124]) ).
fof(f1132,plain,
( ! [X0] : true = ifeq(true,true,ifeq(holds(clear(d),X0),true,holds(clear(d),do(pickup(a),X0)),true),true)
| ~ spl1_41 ),
inference(superposition,[],[f11,f1126]) ).
fof(f1135,plain,
( ! [X0] : true = ifeq(holds(clear(d),X0),true,holds(clear(d),do(pickup(a),X0)),true)
| ~ spl1_41 ),
inference(forward_demodulation,[],[f1132,f1]) ).
fof(f1398,plain,
( true = ifeq(true,true,ifeq(holds(clear(a),do(putdown(c,table),do(pickup(c),s0))),true,holds(holding(a),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))),true),true)
| ~ spl1_8
| ~ spl1_26 ),
inference(superposition,[],[f432,f769]) ).
fof(f1407,plain,
( true = ifeq(holds(clear(a),do(putdown(c,table),do(pickup(c),s0))),true,holds(holding(a),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))),true)
| ~ spl1_8
| ~ spl1_26 ),
inference(forward_demodulation,[],[f1398,f1]) ).
fof(f1470,definition,
( spl1_45
<=> true = holds(clear(a),do(pickup(c),s0)) ),
introduced(definition,[new_symbols(definition,[spl1_45])],[avatar_definition]) ).
fof(f1472,plain,
( true = holds(clear(a),do(pickup(c),s0))
| ~ spl1_45 ),
inference(avatar_component_clause,[],[f1470]) ).
fof(f1473,plain,
( spl1_45
| ~ spl1_3
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f217,f153,f82,f1470]) ).
fof(f1483,plain,
( ! [X0] : true = ifeq(true,true,holds(clear(a),do(putdown(X0,table),do(pickup(c),s0))),true)
| ~ spl1_8
| ~ spl1_45 ),
inference(superposition,[],[f430,f1472]) ).
fof(f1516,plain,
( ! [X0] : true = holds(clear(a),do(putdown(X0,table),do(pickup(c),s0)))
| ~ spl1_8
| ~ spl1_45 ),
inference(forward_demodulation,[],[f1483,f1]) ).
fof(f1529,plain,
( true = ifeq(true,true,holds(holding(a),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))),true)
| ~ spl1_8
| ~ spl1_26
| ~ spl1_45 ),
inference(backward_demodulation,[],[f1407,f1516]) ).
fof(f1534,plain,
( true = holds(holding(a),do(pickup(a),do(putdown(c,table),do(pickup(c),s0))))
| ~ spl1_8
| ~ spl1_26
| ~ spl1_45 ),
inference(forward_demodulation,[],[f1529,f1]) ).
fof(f1538,definition,
( spl1_46
<=> true = holds(holding(a),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))) ),
introduced(definition,[new_symbols(definition,[spl1_46])],[avatar_definition]) ).
fof(f1540,plain,
( true = holds(holding(a),do(pickup(a),do(putdown(c,table),do(pickup(c),s0))))
| ~ spl1_46 ),
inference(avatar_component_clause,[],[f1538]) ).
fof(f1541,plain,
( spl1_46
| ~ spl1_8
| ~ spl1_26
| ~ spl1_45 ),
inference(avatar_split_clause,[],[f1534,f1470,f767,f133,f1538]) ).
fof(f1750,plain,
( ! [X0] : true = ifeq(true,true,holds(clear(d),do(pickup(a),do(putdown(X0,table),do(pickup(c),s0)))),true)
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41 ),
inference(superposition,[],[f1135,f508]) ).
fof(f1778,plain,
( ! [X0] : true = holds(clear(d),do(pickup(a),do(putdown(X0,table),do(pickup(c),s0))))
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41 ),
inference(forward_demodulation,[],[f1750,f1]) ).
fof(f1992,plain,
( true = ifeq(true,true,ifeq(holds(clear(d),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))),true,holds(sF0,do(putdown(a,d),do(pickup(a),do(putdown(c,table),do(pickup(c),s0))))),true),true)
| ~ spl1_1
| ~ spl1_46 ),
inference(superposition,[],[f73,f1540]) ).
fof(f2011,plain,
( true = ifeq(holds(clear(d),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))),true,holds(sF0,do(putdown(a,d),do(pickup(a),do(putdown(c,table),do(pickup(c),s0))))),true)
| ~ spl1_1
| ~ spl1_46 ),
inference(forward_demodulation,[],[f1992,f1]) ).
fof(f2014,plain,
( true = ifeq(true,true,holds(sF0,do(putdown(a,d),do(pickup(a),do(putdown(c,table),do(pickup(c),s0))))),true)
| ~ spl1_1
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41
| ~ spl1_46 ),
inference(forward_demodulation,[],[f2011,f1778]) ).
fof(f2017,plain,
( true = holds(sF0,do(putdown(a,d),do(pickup(a),do(putdown(c,table),do(pickup(c),s0)))))
| ~ spl1_1
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41
| ~ spl1_46 ),
inference(forward_demodulation,[],[f2014,f1]) ).
fof(f2020,plain,
( $false
| ~ spl1_1
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41
| ~ spl1_46 ),
inference(forward_subsumption_resolution,[],[f2017,f66]) ).
fof(f2021,plain,
( ~ spl1_1
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41
| ~ spl1_46 ),
inference(avatar_contradiction_clause,[],[f2020]) ).
cnf(s1,plain,
spl1_1,
inference(sat_conversion,[],[f71]) ).
cnf(s3,plain,
spl1_3,
inference(sat_conversion,[],[f85]) ).
cnf(s4,plain,
spl1_4,
inference(sat_conversion,[],[f90]) ).
cnf(s7,plain,
spl1_7,
inference(sat_conversion,[],[f124]) ).
cnf(s8,plain,
spl1_8,
inference(sat_conversion,[],[f136]) ).
cnf(s9,plain,
spl1_9,
inference(sat_conversion,[],[f151]) ).
cnf(s10,plain,
spl1_10,
inference(sat_conversion,[],[f156]) ).
cnf(s13,plain,
spl1_13,
inference(sat_conversion,[],[f293]) ).
cnf(s14,plain,
( ~ spl1_7
| ~ spl1_13
| spl1_14 ),
inference(sat_conversion,[],[f326]) ).
cnf(s19,plain,
spl1_19,
inference(sat_conversion,[],[f463]) ).
cnf(s20,plain,
( ~ spl1_7
| ~ spl1_13
| ~ spl1_19
| spl1_20 ),
inference(sat_conversion,[],[f482]) ).
cnf(s26,plain,
( ~ spl1_14
| spl1_26 ),
inference(sat_conversion,[],[f770]) ).
cnf(s41,plain,
( ~ spl1_4
| spl1_41 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s45,plain,
( ~ spl1_3
| ~ spl1_10
| spl1_45 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s46,plain,
( ~ spl1_8
| ~ spl1_26
| ~ spl1_45
| spl1_46 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s56,plain,
( ~ spl1_1
| ~ spl1_9
| ~ spl1_20
| ~ spl1_41
| ~ spl1_46 ),
inference(sat_conversion,[],[f2021]) ).
cnf(s62,plain,
spl1_20,
inference(rat,[],[s20,s13,s19,s7]) ).
cnf(s64,plain,
spl1_14,
inference(rat,[],[s14,s13,s7]) ).
cnf(s72,plain,
spl1_26,
inference(rat,[],[s26,s64]) ).
cnf(s83,plain,
spl1_41,
inference(rat,[],[s41,s4]) ).
cnf(s84,plain,
spl1_45,
inference(rat,[],[s45,s10,s3]) ).
cnf(s86,plain,
spl1_46,
inference(rat,[],[s46,s72,s8,s84]) ).
cnf(s89,plain,
~ spl1_1,
inference(rat,[],[s56,s83,s62,s9,s86]) ).
cnf(s94,plain,
$false,
inference(rat,[],[s1,s89]) ).
fof(f2023,plain,
$false,
inference(avatar_sat_refutation,[],[s94]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PLA007-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 22:14:03 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.44 Running first-order theorem proving
% 0.15/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.22/3.38 % (3043488)Detected a unit-equality problem, will run specialized UEQ schedule.
% 15.22/3.38 % (3043498)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3667331978:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 15.22/3.38 % (3043493)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=925918508:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 15.22/3.38 % (3043494)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=319943764:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 15.22/3.38 % (3043496)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1866772369:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 15.22/3.38 % (3043495)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2810173383:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 15.22/3.38 % (3043499)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3672040155:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 15.22/3.38 % (3043497)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2968405086:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 15.22/3.38 % (3043498)Instruction limit reached!
% 15.22/3.38 % (3043498)------------------------------
% 15.22/3.38 % (3043498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043498)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043498)Termination reason: Instruction limit
% 15.22/3.38 % (3043498)Termination phase: Saturation
% 15.22/3.38 % (3043498)Time elapsed: 0.135 s
% 15.22/3.38 % (3043498)Peak memory usage: 94 MB
% 15.22/3.38 % (3043498)Instructions burned: 257 (million)
% 15.22/3.38 % (3043496)Instruction limit reached!
% 15.22/3.38 % (3043496)------------------------------
% 15.22/3.38 % (3043496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043496)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043496)Termination reason: Instruction limit
% 15.22/3.38 % (3043496)Termination phase: Saturation
% 15.22/3.38 % (3043496)Time elapsed: 0.126 s
% 15.22/3.38 % (3043496)Peak memory usage: 89 MB
% 15.22/3.38 % (3043496)Instructions burned: 136 (million)
% 15.22/3.38 % (3043497)Instruction limit reached!
% 15.22/3.38 % (3043497)------------------------------
% 15.22/3.38 % (3043497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043497)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043497)Termination reason: Instruction limit
% 15.22/3.38 % (3043497)Termination phase: Saturation
% 15.22/3.38 % (3043497)Time elapsed: 0.168 s
% 15.22/3.38 % (3043497)Peak memory usage: 89 MB
% 15.22/3.38 % (3043497)Instructions burned: 182 (million)
% 15.22/3.38 % (3043507)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1106861444:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 15.22/3.38 % (3043508)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4100778137:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 15.22/3.38 % (3043509)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1338414791:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 15.22/3.38 % (3043509)Instruction limit reached!
% 15.22/3.38 % (3043509)------------------------------
% 15.22/3.38 % (3043509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043509)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043509)Termination reason: Instruction limit
% 15.22/3.38 % (3043509)Termination phase: Saturation
% 15.22/3.38 % (3043509)Time elapsed: 0.170 s
% 15.22/3.38 % (3043509)Peak memory usage: 88 MB
% 15.22/3.38 % (3043509)Instructions burned: 215 (million)
% 15.22/3.38 % (3043513)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2534404429:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/317Mi)
% 15.22/3.38 % (3043499)Instruction limit reached!
% 15.22/3.38 % (3043499)------------------------------
% 15.22/3.38 % (3043499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043499)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043499)Termination reason: Instruction limit
% 15.22/3.38 % (3043499)Termination phase: Saturation
% 15.22/3.38 % (3043499)Time elapsed: 0.977 s
% 15.22/3.38 % (3043499)Peak memory usage: 104 MB
% 15.22/3.38 % (3043499)Instructions burned: 1187 (million)
% 15.22/3.38 % (3043513)Instruction limit reached!
% 15.22/3.38 % (3043513)------------------------------
% 15.22/3.38 % (3043513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043513)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043513)Termination reason: Instruction limit
% 15.22/3.38 % (3043513)Termination phase: Saturation
% 15.22/3.38 % (3043513)Time elapsed: 0.302 s
% 15.22/3.38 % (3043513)Peak memory usage: 95 MB
% 15.22/3.38 % (3043513)Instructions burned: 317 (million)
% 15.22/3.38 % (3043515)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=677140729:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/12125Mi)
% 15.22/3.38 % (3043493)First to succeed.
% 15.22/3.38 % (3043493)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3043488"
% 15.22/3.38 % (3043507)Instruction limit reached!
% 15.22/3.38 % (3043507)------------------------------
% 15.22/3.38 % (3043507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.22/3.38 % (3043507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.22/3.38 % (3043507)CaDiCaL version: 2.1.3
% 15.22/3.38 % (3043507)Termination reason: Instruction limit
% 15.22/3.38 % (3043507)Termination phase: Saturation
% 15.22/3.38 % (3043507)Time elapsed: 1.147 s
% 15.22/3.38 % (3043507)Peak memory usage: 142 MB
% 15.22/3.38 % (3043507)Instructions burned: 2052 (million)
% 15.22/3.38 % (3043516)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2611504391:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2984 on theBenchmark for (2984ds/2836Mi)
% 15.22/3.38 % (3043518)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3797793167:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2981 on theBenchmark for (2981ds/14534Mi)
% 15.22/3.38 % (3043493)Refutation found. Thanks to Tanya!
% 15.22/3.38 % SZS status Unsatisfiable for theBenchmark
% 15.22/3.38 % SZS output start Proof for theBenchmark
% See solution above
% 16.32/3.74 % (3043493)------------------------------
% 16.32/3.74 % (3043493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.74 % (3043493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.74 % (3043493)CaDiCaL version: 2.1.3
% 16.32/3.74 % (3043493)Termination reason: Refutation
% 16.32/3.74 % (3043493)Time elapsed: 1.464 s
% 16.32/3.74 % (3043493)Peak memory usage: 133 MB
% 16.32/3.74 % (3043493)Instructions burned: 1386 (million)
% 16.32/3.74 % (3043493)------------------------------
% 16.32/3.74 % (3043493)------------------------------
% 16.32/3.74 % (3043488)Success in time 2.186 s
% 16.32/3.74 % Vampire exiting
%------------------------------------------------------------------------------