%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PLA017-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 01:58:41 PM UTC 2026
% Result : Unsatisfiable 0.17s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PLA017-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n005.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 03:32:18 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.62 % Refutation found
% 0.17/0.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.17/0.62 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.62 fof(f1,axiom,(
% 0.17/0.62 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f3,axiom,(
% 0.17/0.62 (![X,State]: (ifeq(differ(X,table),true,ifeq(holds(empty,State),true,ifeq(holds(clear(X),State),true,holds(holding(X),do(pickup(X),State)),true),true),true) = true ))),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f6,axiom,(
% 0.17/0.62 (![X,Z,State]: (ifeq(differ(X,Z),true,ifeq(holds(clear(X),State),true,holds(clear(X),do(pickup(Z),State)),true),true) = true ))),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f8,axiom,(
% 0.17/0.62 (![X,State,Y]: (ifeq(holds(holding(X),State),true,ifeq(holds(clear(Y),State),true,holds(on(X,Y),do(putdown(X,Y),State)),true),true) = true ))),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f12,axiom,(
% 0.17/0.62 (![Y,X]: (ifeq(differ(Y,X),true,differ(X,Y),true) = true ))),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f14,axiom,(
% 0.17/0.62 differ(a,c) = true ),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f16,axiom,(
% 0.17/0.62 differ(a,table) = true ),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f27,axiom,(
% 0.17/0.62 holds(clear(a),s0) = true ),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f29,axiom,(
% 0.17/0.62 holds(clear(c),s0) = true ),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f30,axiom,(
% 0.17/0.62 holds(empty,s0) = true ),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f32,negated_conjecture,(
% 0.17/0.62 (![State]: (holds(on(a,c),State) != true ))),
% 0.17/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.62 fof(f33,plain,(
% 0.17/0.62 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f1])).
% 0.17/0.62 fof(f35,plain,(
% 0.17/0.62 ![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)),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.62 fof(f38,plain,(
% 0.17/0.62 ![X0,X1,X2]: (ifeq(differ(X0,X1),true,ifeq(holds(clear(X0),X2),true,holds(clear(X0),do(pickup(X1),X2)),true),true)=true)),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.62 fof(f40,plain,(
% 0.17/0.62 ![X0,X1,X2]: (ifeq(holds(holding(X0),X1),true,ifeq(holds(clear(X2),X1),true,holds(on(X0,X2),do(putdown(X0,X2),X1)),true),true)=true)),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.62 fof(f44,plain,(
% 0.17/0.62 ![X0,X1]: (ifeq(differ(X0,X1),true,differ(X1,X0),true)=true)),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.62 fof(f46,plain,(
% 0.17/0.62 differ(a,c)=true),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f14])).
% 0.17/0.62 fof(f48,plain,(
% 0.17/0.62 differ(a,table)=true),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f16])).
% 0.17/0.62 fof(f59,plain,(
% 0.17/0.62 holds(clear(a),s0)=true),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f27])).
% 0.17/0.62 fof(f61,plain,(
% 0.17/0.62 holds(clear(c),s0)=true),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f29])).
% 0.17/0.62 fof(f62,plain,(
% 0.17/0.62 holds(empty,s0)=true),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f30])).
% 0.17/0.62 fof(f64,plain,(
% 0.17/0.62 ![X0]: (~holds(on(a,c),X0)=true)),
% 0.17/0.62 inference(cnf_transformation,[status(thm)],[f32])).
% 0.17/0.62 fof(f65,definition,(
% 0.17/0.62 sF1_fnc=on(a,c)),
% 0.17/0.62 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.17/0.62 fof(f66,definition,(
% 0.17/0.62 ![X0]: (sF0_fnc(X0)=holds(sF1_fnc,X0))),
% 0.17/0.62 introduced(definition,[new_symbols(definition,[sF0_fnc(X0)])],[function_definition])).
% 0.17/0.62 fof(f67,plain,(
% 0.17/0.62 ![X0]: (~sF0_fnc(X0)=true)),
% 0.17/0.62 inference(definition_folding,[],[f64,f66,f65])).
% 0.17/0.62 fof(f110,plain,(
% 0.17/0.62 ifeq(differ(a,table),true,ifeq(holds(empty,s0),true,ifeq(true,true,holds(holding(a),do(pickup(a),s0)),true),true),true)=true),
% 0.17/0.62 inference(paramodulation,[status(thm)],[f59,f35])).
% 0.17/0.62 fof(f122,plain,(
% 0.17/0.62 ifeq(true,true,ifeq(holds(empty,s0),true,ifeq(true,true,holds(holding(a),do(pickup(a),s0)),true),true),true)=true),
% 0.17/0.62 inference(forward_demodulation,[status(thm)],[f48,f110])).
% 0.17/0.62 fof(f123,plain,(
% 0.17/0.62 ifeq(holds(empty,s0),true,ifeq(true,true,holds(holding(a),do(pickup(a),s0)),true),true)=true),
% 0.17/0.62 inference(forward_demodulation,[status(thm)],[f33,f122])).
% 0.17/0.64 fof(f124,plain,(
% 0.17/0.64 ifeq(true,true,ifeq(true,true,holds(holding(a),do(pickup(a),s0)),true),true)=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f62,f123])).
% 0.17/0.64 fof(f125,plain,(
% 0.17/0.64 ifeq(true,true,holds(holding(a),do(pickup(a),s0)),true)=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f124])).
% 0.17/0.64 fof(f126,plain,(
% 0.17/0.64 holds(holding(a),do(pickup(a),s0))=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f125])).
% 0.17/0.64 fof(f474,plain,(
% 0.17/0.64 ifeq(true,true,differ(c,a),true)=true),
% 0.17/0.64 inference(paramodulation,[status(thm)],[f46,f44])).
% 0.17/0.64 fof(f494,plain,(
% 0.17/0.64 differ(c,a)=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f474])).
% 0.17/0.64 fof(f521,plain,(
% 0.17/0.64 ![X0]: (ifeq(differ(c,X0),true,ifeq(true,true,holds(clear(c),do(pickup(X0),s0)),true),true)=true)),
% 0.17/0.64 inference(paramodulation,[status(thm)],[f61,f38])).
% 0.17/0.64 fof(f543,plain,(
% 0.17/0.64 ![X0]: (ifeq(differ(c,X0),true,holds(clear(c),do(pickup(X0),s0)),true)=true)),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f521])).
% 0.17/0.64 fof(f565,plain,(
% 0.17/0.64 ![X0]: (ifeq(holds(holding(a),X0),true,ifeq(holds(clear(c),X0),true,holds(sF1_fnc,do(putdown(a,c),X0)),true),true)=true)),
% 0.17/0.64 inference(paramodulation,[status(thm)],[f65,f40])).
% 0.17/0.64 fof(f572,plain,(
% 0.17/0.64 ![X0]: (ifeq(holds(holding(a),X0),true,ifeq(holds(clear(c),X0),true,sF0_fnc(do(putdown(a,c),X0)),true),true)=true)),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f66,f565])).
% 0.17/0.64 fof(f4119,plain,(
% 0.17/0.64 ifeq(true,true,holds(clear(c),do(pickup(a),s0)),true)=true),
% 0.17/0.64 inference(paramodulation,[status(thm)],[f494,f543])).
% 0.17/0.64 fof(f4124,plain,(
% 0.17/0.64 holds(clear(c),do(pickup(a),s0))=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f4119])).
% 0.17/0.64 fof(f4193,plain,(
% 0.17/0.64 ifeq(holds(holding(a),do(pickup(a),s0)),true,ifeq(true,true,sF0_fnc(do(putdown(a,c),do(pickup(a),s0))),true),true)=true),
% 0.17/0.64 inference(paramodulation,[status(thm)],[f4124,f572])).
% 0.17/0.64 fof(f4219,plain,(
% 0.17/0.64 ifeq(true,true,ifeq(true,true,sF0_fnc(do(putdown(a,c),do(pickup(a),s0))),true),true)=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f126,f4193])).
% 0.17/0.64 fof(f4220,plain,(
% 0.17/0.64 ifeq(true,true,sF0_fnc(do(putdown(a,c),do(pickup(a),s0))),true)=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f4219])).
% 0.17/0.64 fof(f4221,plain,(
% 0.17/0.64 sF0_fnc(do(putdown(a,c),do(pickup(a),s0)))=true),
% 0.17/0.64 inference(forward_demodulation,[status(thm)],[f33,f4220])).
% 0.17/0.64 fof(f4222,plain,(
% 0.17/0.64 $false),
% 0.17/0.64 inference(forward_subsumption_resolution,[status(thm)],[f4221,f67])).
% 0.17/0.64 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.64 % Elapsed time: 0.203997 seconds
% 0.17/0.64 % CPU time: 1.415252 seconds
% 0.17/0.64 % Total memory used: 34.867 MB
% 0.17/0.64 % Net memory used: 34.650 MB
%------------------------------------------------------------------------------