%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PLA017-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 08:20:23 AM UTC 2026
% Result : Unsatisfiable 8.01s 1.50s
% Output : CNFRefutation 8.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 12
% Syntax : Number of formulae : 118 ( 118 unt; 0 def)
% Number of atoms : 118 ( 117 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-4 aty)
% Number of variables : 185 ( 5 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(pickup_1,axiom,
! [VAR_0,VAR_1] : ifeq(differ(VAR_0,table),true,ifeq(holds(empty,VAR_1),true,ifeq(holds(clear(VAR_0),VAR_1),true,holds(holding(VAR_0),do(pickup(VAR_0),VAR_1)),true),true),true) = true,
file('theBenchmark.p',pickup_1) ).
cnf(c_3,plain,
ifeq(differ(A,table),true,ifeq(holds(empty,B),true,ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(clausify,[status(thm)],[pickup_1]) ).
fof(pickup_4,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(differ(VAR_0,VAR_1),true,ifeq(holds(clear(VAR_0),VAR_2),true,holds(clear(VAR_0),do(pickup(VAR_1),VAR_2)),true),true) = true,
file('theBenchmark.p',pickup_4) ).
cnf(c_6,plain,
ifeq(differ(A,B),true,ifeq(holds(clear(A),C),true,holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(clausify,[status(thm)],[pickup_4]) ).
fof(putdown_2,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(holds(holding(VAR_0),VAR_1),true,ifeq(holds(clear(VAR_2),VAR_1),true,holds(on(VAR_0,VAR_2),do(putdown(VAR_0,VAR_2),VAR_1)),true),true) = true,
file('theBenchmark.p',putdown_2) ).
cnf(c_8,plain,
ifeq(holds(holding(A),B),true,ifeq(holds(clear(C),B),true,holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(clausify,[status(thm)],[putdown_2]) ).
fof(symmetry_of_differ,axiom,
! [VAR_0,VAR_1] : ifeq(differ(VAR_0,VAR_1),true,differ(VAR_1,VAR_0),true) = true,
file('theBenchmark.p',symmetry_of_differ) ).
cnf(c_12,plain,
ifeq(differ(A,B),true,differ(B,A),true) = true,
inference(clausify,[status(thm)],[symmetry_of_differ]) ).
fof(differ_a_b,axiom,
differ(a,b) = true,
file('theBenchmark.p',differ_a_b) ).
cnf(c_13,plain,
differ(a,b) = true,
inference(clausify,[status(thm)],[differ_a_b]) ).
cnf(c_14,plain,
true = differ(a,b),
inference(copy,[status(thm)],[c_13]) ).
fof(differ_a_c,axiom,
differ(a,c) = true,
file('theBenchmark.p',differ_a_c) ).
cnf(c_15,plain,
differ(a,c) = true,
inference(clausify,[status(thm)],[differ_a_c]) ).
cnf(c_16,plain,
differ(a,c) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_15]) ).
fof(differ_a_table,axiom,
differ(a,table) = true,
file('theBenchmark.p',differ_a_table) ).
cnf(c_19,plain,
differ(a,table) = true,
inference(clausify,[status(thm)],[differ_a_table]) ).
cnf(c_3267,plain,
differ(a,table) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_19]) ).
cnf(c_20,plain,
differ(a,b) = differ(a,table),
inference(copy,[status(thm)],[c_3267]) ).
fof(initial_state5,axiom,
holds(clear(a),s0) = true,
file('theBenchmark.p',initial_state5) ).
cnf(c_41,plain,
holds(clear(a),s0) = true,
inference(clausify,[status(thm)],[initial_state5]) ).
cnf(c_3268,plain,
holds(clear(a),s0) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_41]) ).
cnf(c_42,plain,
holds(clear(a),s0) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3268]) ).
fof(initial_state7,axiom,
holds(clear(c),s0) = true,
file('theBenchmark.p',initial_state7) ).
cnf(c_45,plain,
holds(clear(c),s0) = true,
inference(clausify,[status(thm)],[initial_state7]) ).
cnf(c_3269,plain,
holds(clear(c),s0) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_45]) ).
cnf(c_46,plain,
holds(clear(c),s0) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3269]) ).
fof(initial_state8,axiom,
holds(empty,s0) = true,
file('theBenchmark.p',initial_state8) ).
cnf(c_47,plain,
holds(empty,s0) = true,
inference(clausify,[status(thm)],[initial_state8]) ).
cnf(c_3270,plain,
holds(empty,s0) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_47]) ).
cnf(c_3271,plain,
holds(empty,s0) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3270]) ).
cnf(c_48,plain,
differ(a,table) = holds(empty,s0),
inference(copy,[status(thm)],[c_3271]) ).
fof(prove_AC,axiom,
! [VAR_0] : holds(on(a,c),VAR_0) != true,
file('theBenchmark.p',prove_AC) ).
cnf(c_51,plain,
holds(on(a,c),A) != true,
inference(clausify,[status(thm)],[prove_AC]) ).
cnf(c_3272,plain,
holds(on(a,c),A) != differ(a,b),
inference(paramod,[status(thm)],[c_14,c_51]) ).
cnf(c_3273,plain,
holds(on(a,c),A) != differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3272]) ).
cnf(c_52,plain,
holds(on(a,c),A) != holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3273]) ).
cnf(c_3274,plain,
ifeq(differ(A,B),differ(a,b),differ(B,A),true) = true,
inference(paramod,[status(thm)],[c_14,c_12]) ).
cnf(c_3275,plain,
ifeq(differ(A,B),differ(a,table),differ(B,A),true) = true,
inference(paramod,[status(thm)],[c_20,c_3274]) ).
cnf(c_3276,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),true) = true,
inference(paramod,[status(thm)],[c_48,c_3275]) ).
cnf(c_3277,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),differ(a,b)) = true,
inference(paramod,[status(thm)],[c_14,c_3276]) ).
cnf(c_3278,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),differ(a,table)) = true,
inference(paramod,[status(thm)],[c_20,c_3277]) ).
cnf(c_3279,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),holds(empty,s0)) = true,
inference(paramod,[status(thm)],[c_48,c_3278]) ).
cnf(c_3280,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),holds(empty,s0)) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_3279]) ).
cnf(c_3281,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),holds(empty,s0)) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3280]) ).
cnf(c_53,plain,
ifeq(differ(A,B),holds(empty,s0),differ(B,A),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3281]) ).
cnf(c_3282,plain,
ifeq(holds(holding(A),B),differ(a,b),ifeq(holds(clear(C),B),true,holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_8]) ).
cnf(c_3283,plain,
ifeq(holds(holding(A),B),differ(a,table),ifeq(holds(clear(C),B),true,holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3282]) ).
cnf(c_3284,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),true,holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3283]) ).
cnf(c_3285,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),differ(a,b),holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_3284]) ).
cnf(c_3286,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),differ(a,table),holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3285]) ).
cnf(c_3287,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3286]) ).
cnf(c_3288,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),differ(a,b)),true) = true,
inference(paramod,[status(thm)],[c_14,c_3287]) ).
cnf(c_3289,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),differ(a,table)),true) = true,
inference(paramod,[status(thm)],[c_20,c_3288]) ).
cnf(c_3290,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),true) = true,
inference(paramod,[status(thm)],[c_48,c_3289]) ).
cnf(c_3291,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),differ(a,b)) = true,
inference(paramod,[status(thm)],[c_14,c_3290]) ).
cnf(c_3292,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),differ(a,table)) = true,
inference(paramod,[status(thm)],[c_20,c_3291]) ).
cnf(c_3293,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),holds(empty,s0)) = true,
inference(paramod,[status(thm)],[c_48,c_3292]) ).
cnf(c_3294,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),holds(empty,s0)) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_3293]) ).
cnf(c_3295,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),holds(empty,s0)) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3294]) ).
cnf(c_57,plain,
ifeq(holds(holding(A),B),holds(empty,s0),ifeq(holds(clear(C),B),holds(empty,s0),holds(on(A,C),do(putdown(A,C),B)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3295]) ).
cnf(c_3296,plain,
ifeq(differ(A,B),differ(a,b),ifeq(holds(clear(A),C),true,holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_6]) ).
cnf(c_3297,plain,
ifeq(differ(A,B),differ(a,table),ifeq(holds(clear(A),C),true,holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3296]) ).
cnf(c_3298,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),true,holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3297]) ).
cnf(c_3299,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),differ(a,b),holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_3298]) ).
cnf(c_3300,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),differ(a,table),holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3299]) ).
cnf(c_3301,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3300]) ).
cnf(c_3302,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),differ(a,b)),true) = true,
inference(paramod,[status(thm)],[c_14,c_3301]) ).
cnf(c_3303,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),differ(a,table)),true) = true,
inference(paramod,[status(thm)],[c_20,c_3302]) ).
cnf(c_3304,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),true) = true,
inference(paramod,[status(thm)],[c_48,c_3303]) ).
cnf(c_3305,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),differ(a,b)) = true,
inference(paramod,[status(thm)],[c_14,c_3304]) ).
cnf(c_3306,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),differ(a,table)) = true,
inference(paramod,[status(thm)],[c_20,c_3305]) ).
cnf(c_3307,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),holds(empty,s0)) = true,
inference(paramod,[status(thm)],[c_48,c_3306]) ).
cnf(c_3308,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),holds(empty,s0)) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_3307]) ).
cnf(c_3309,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),holds(empty,s0)) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3308]) ).
cnf(c_59,plain,
ifeq(differ(A,B),holds(empty,s0),ifeq(holds(clear(A),C),holds(empty,s0),holds(clear(A),do(pickup(B),C)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3309]) ).
cnf(c_3310,plain,
ifeq(differ(A,table),differ(a,b),ifeq(holds(empty,B),true,ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_3]) ).
cnf(c_3311,plain,
ifeq(differ(A,table),differ(a,table),ifeq(holds(empty,B),true,ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3310]) ).
cnf(c_3312,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),true,ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3311]) ).
cnf(c_3313,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),differ(a,b),ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_3312]) ).
cnf(c_3314,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),differ(a,table),ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3313]) ).
cnf(c_3315,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),true,holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3314]) ).
cnf(c_3316,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),differ(a,b),holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_3315]) ).
cnf(c_3317,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),differ(a,table),holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3316]) ).
cnf(c_3318,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3317]) ).
cnf(c_3319,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),differ(a,b)),true),true) = true,
inference(paramod,[status(thm)],[c_14,c_3318]) ).
cnf(c_3320,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),differ(a,table)),true),true) = true,
inference(paramod,[status(thm)],[c_20,c_3319]) ).
cnf(c_3321,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),true),true) = true,
inference(paramod,[status(thm)],[c_48,c_3320]) ).
cnf(c_3322,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),differ(a,b)),true) = true,
inference(paramod,[status(thm)],[c_14,c_3321]) ).
cnf(c_3323,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),differ(a,table)),true) = true,
inference(paramod,[status(thm)],[c_20,c_3322]) ).
cnf(c_3324,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),true) = true,
inference(paramod,[status(thm)],[c_48,c_3323]) ).
cnf(c_3325,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),differ(a,b)) = true,
inference(paramod,[status(thm)],[c_14,c_3324]) ).
cnf(c_3326,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),differ(a,table)) = true,
inference(paramod,[status(thm)],[c_20,c_3325]) ).
cnf(c_3327,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),holds(empty,s0)) = true,
inference(paramod,[status(thm)],[c_48,c_3326]) ).
cnf(c_3328,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),holds(empty,s0)) = differ(a,b),
inference(paramod,[status(thm)],[c_14,c_3327]) ).
cnf(c_3329,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),holds(empty,s0)) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_3328]) ).
cnf(c_62,plain,
ifeq(differ(A,table),holds(empty,s0),ifeq(holds(empty,B),holds(empty,s0),ifeq(holds(clear(A),B),holds(empty,s0),holds(holding(A),do(pickup(A),B)),holds(empty,s0)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3329]) ).
cnf(c_3330,plain,
differ(a,c) = differ(a,table),
inference(paramod,[status(thm)],[c_20,c_16]) ).
cnf(c_65,plain,
differ(a,c) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3330]) ).
cnf(c_67,plain,
holds(clear(c),s0) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_46]) ).
cnf(c_69,plain,
holds(clear(a),s0) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_42]) ).
cnf(c_3331,plain,
ifeq(holds(empty,s0),holds(empty,s0),differ(c,a),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_65,c_53]) ).
cnf(c_104,plain,
differ(c,a) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3331]) ).
cnf(c_3332,plain,
ifeq(differ(c,A),holds(empty,s0),ifeq(holds(empty,s0),holds(empty,s0),holds(clear(c),do(pickup(A),s0)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_67,c_59]) ).
cnf(c_112,plain,
ifeq(differ(c,A),holds(empty,s0),holds(clear(c),do(pickup(A),s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3332]) ).
cnf(c_3333,plain,
ifeq(differ(a,table),holds(empty,s0),ifeq(holds(empty,s0),holds(empty,s0),ifeq(holds(empty,s0),holds(empty,s0),holds(holding(a),do(pickup(a),s0)),holds(empty,s0)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_69,c_62]) ).
cnf(c_3334,plain,
ifeq(holds(empty,s0),holds(empty,s0),ifeq(holds(empty,s0),holds(empty,s0),ifeq(holds(empty,s0),holds(empty,s0),holds(holding(a),do(pickup(a),s0)),holds(empty,s0)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_48,c_3333]) ).
cnf(c_3335,plain,
ifeq(holds(empty,s0),holds(empty,s0),ifeq(holds(empty,s0),holds(empty,s0),holds(holding(a),do(pickup(a),s0)),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3334]) ).
cnf(c_3336,plain,
ifeq(holds(empty,s0),holds(empty,s0),holds(holding(a),do(pickup(a),s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3335]) ).
cnf(c_132,plain,
holds(holding(a),do(pickup(a),s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3336]) ).
cnf(c_3337,plain,
ifeq(holds(empty,s0),holds(empty,s0),ifeq(holds(clear(A),do(pickup(a),s0)),holds(empty,s0),holds(on(a,A),do(putdown(a,A),do(pickup(a),s0))),holds(empty,s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_132,c_57]) ).
cnf(c_223,plain,
ifeq(holds(clear(A),do(pickup(a),s0)),holds(empty,s0),holds(on(a,A),do(putdown(a,A),do(pickup(a),s0))),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3337]) ).
cnf(c_3338,plain,
ifeq(holds(empty,s0),holds(empty,s0),holds(clear(c),do(pickup(a),s0)),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_104,c_112]) ).
cnf(c_572,plain,
holds(clear(c),do(pickup(a),s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3338]) ).
cnf(c_3339,plain,
ifeq(holds(empty,s0),holds(empty,s0),holds(on(a,c),do(putdown(a,c),do(pickup(a),s0))),holds(empty,s0)) = holds(empty,s0),
inference(paramod,[status(thm)],[c_572,c_223]) ).
cnf(c_3265,plain,
holds(on(a,c),do(putdown(a,c),do(pickup(a),s0))) = holds(empty,s0),
inference(paramod,[status(thm)],[c_1,c_3339]) ).
cnf(c_3266,plain,
$false,
inference(resolve,[status(thm)],[c_3265,c_52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA017-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 04:44:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3792207 was started by sandbox on n011,
% 0.09/0.37 % Sat Sep 26 04:44:14 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 8.01/1.50
% 8.01/1.50 % SZS status Unsatisfiable for theBenchmark
% 8.01/1.50
% 8.01/1.50 % Proof 1 at 0.90 (+ 0.15) seconds.
% 8.01/1.50 % Length of proof is 33.
% 8.01/1.50 % Level of proof is 8.
% 8.01/1.50 % Maximum clause weight is 77.000.
% 8.01/1.50 % Given clauses 394.
% 8.01/1.50
% 8.01/1.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------