%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT168-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(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 : Thu Sep 24 01:03:19 PM UTC 2026
% Result : Unsatisfiable 14.50s 2.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT168-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n015.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 20 23:20:21 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 14.50/2.41 % Refutation found
% 14.50/2.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 14.50/2.41 % SZS output start CNFRefutation for theBenchmark
% 14.50/2.41 fof(f3,axiom,(
% 14.50/2.41 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f4,axiom,(
% 14.50/2.41 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f5,axiom,(
% 14.50/2.41 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f6,axiom,(
% 14.50/2.41 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f7,axiom,(
% 14.50/2.41 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f8,axiom,(
% 14.50/2.41 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f9,axiom,(
% 14.50/2.41 (![X,Y,Z]: (meet(join(X,Y),join(X,Z)) = join(X,meet(join(X,Y),meet(join(X,Z),join(Y,meet(X,Z))))) ))),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f10,negated_conjecture,(
% 14.50/2.41 meet(a,join(b,c)) != meet(a,join(b,meet(join(a,b),join(c,meet(a,b))))) ),
% 14.50/2.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.50/2.41 fof(f13,plain,(
% 14.50/2.41 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f3])).
% 14.50/2.41 fof(f14,plain,(
% 14.50/2.41 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f4])).
% 14.50/2.41 fof(f15,plain,(
% 14.50/2.41 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f5])).
% 14.50/2.41 fof(f16,plain,(
% 14.50/2.41 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f6])).
% 14.50/2.41 fof(f17,plain,(
% 14.50/2.41 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f7])).
% 14.50/2.41 fof(f18,plain,(
% 14.50/2.41 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f8])).
% 14.50/2.41 fof(f19,plain,(
% 14.50/2.41 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(join(X0,X1),meet(join(X0,X2),join(X1,meet(X0,X2))))))),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f9])).
% 14.50/2.41 fof(f20,plain,(
% 14.50/2.41 ~meet(a,join(b,c))=meet(a,join(b,meet(join(a,b),join(c,meet(a,b)))))),
% 14.50/2.41 inference(cnf_transformation,[status(thm)],[f10])).
% 14.50/2.41 fof(f38,plain,(
% 14.50/2.41 ~meet(a,join(b,c))=meet(a,join(b,meet(join(a,b),join(c,meet(b,a)))))),
% 14.50/2.41 inference(paramodulation,[status(thm)],[f15,f20])).
% 14.50/2.41 fof(f39,plain,(
% 14.50/2.41 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 14.50/2.41 inference(paramodulation,[status(thm)],[f15,f14])).
% 14.50/2.41 fof(f47,plain,(
% 14.50/2.41 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 14.50/2.41 inference(paramodulation,[status(thm)],[f16,f13])).
% 14.50/2.41 fof(f60,plain,(
% 14.50/2.41 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 14.50/2.41 inference(paramodulation,[status(thm)],[f14,f47])).
% 14.50/2.41 fof(f68,plain,(
% 14.50/2.41 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,X1))),
% 14.50/2.41 inference(forward_demodulation,[status(thm)],[f17,f60])).
% 14.50/2.41 fof(f72,plain,(
% 14.50/2.41 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 14.50/2.41 inference(paramodulation,[status(thm)],[f15,f17])).
% 14.50/2.41 fof(f93,plain,(
% 14.50/2.41 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(join(X0,X1),X2))))),
% 14.50/2.41 inference(paramodulation,[status(thm)],[f14,f18])).
% 14.50/2.42 fof(f94,plain,(
% 14.50/2.42 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 14.50/2.42 inference(paramodulation,[status(thm)],[f16,f18])).
% 14.50/2.42 fof(f108,plain,(
% 14.50/2.42 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,join(X1,X2)))=join(X0,X1))),
% 14.50/2.42 inference(paramodulation,[status(thm)],[f18,f13])).
% 14.50/2.42 fof(f119,plain,(
% 14.50/2.42 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(join(X1,X0),meet(join(X0,X2),join(X1,meet(X0,X2))))))),
% 14.50/2.42 inference(paramodulation,[status(thm)],[f16,f19])).
% 14.50/2.42 fof(f125,plain,(
% 14.50/2.42 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(X2,X0)))=join(X0,meet(join(X0,X1),meet(X0,join(X1,meet(X0,meet(X2,X0)))))))),
% 14.50/2.42 inference(paramodulation,[status(thm)],[f39,f19])).
% 14.50/2.42 fof(f176,plain,(
% 14.50/2.42 ![X0,X1,X2]: (meet(join(X0,X1),X0)=join(X0,meet(join(X0,X1),meet(X0,join(X1,meet(X0,meet(X2,X0)))))))),
% 14.50/2.42 inference(forward_demodulation,[status(thm)],[f39,f125])).
% 14.50/2.42 fof(f177,plain,(
% 14.50/2.42 ![X0,X1,X2]: (meet(join(X0,X1),X0)=join(X0,meet(join(X0,X1),meet(X0,join(X1,meet(X0,X2))))))),
% 14.50/2.42 inference(forward_demodulation,[status(thm)],[f68,f176])).
% 14.50/2.46 fof(f206,plain,(
% 14.50/2.46 ~meet(a,join(b,c))=meet(a,join(b,meet(join(b,a),join(c,meet(b,a)))))),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f16,f38])).
% 14.50/2.46 fof(f372,plain,(
% 14.50/2.46 ![X0,X1,X2]: (join(X0,meet(X1,meet(X0,X2)))=X0)),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f72,f14])).
% 14.50/2.46 fof(f408,plain,(
% 14.50/2.46 ![X0,X1]: (meet(join(X0,X1),X0)=X0)),
% 14.50/2.46 inference(backward_demodulation,[status(thm)],[f372,f177])).
% 14.50/2.46 fof(f420,plain,(
% 14.50/2.46 ![X0,X1]: (meet(join(X0,X1),X1)=X1)),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f16,f408])).
% 14.50/2.46 fof(f466,plain,(
% 14.50/2.46 ![X0,X1,X2]: (meet(X0,meet(X1,join(X2,X0)))=meet(X1,X0))),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f420,f72])).
% 14.50/2.46 fof(f2389,plain,(
% 14.50/2.46 ![X0,X1,X2,X3]: (join(X0,X1)=join(X1,join(meet(X2,meet(X1,X3)),X0)))),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f372,f94])).
% 14.50/2.46 fof(f2391,plain,(
% 14.50/2.46 ![X0,X1,X2,X3]: (join(X0,meet(X1,meet(X0,X2)))=join(X0,join(meet(X1,meet(X0,X2)),meet(X0,X3))))),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f372,f93])).
% 14.50/2.46 fof(f2428,plain,(
% 14.50/2.46 ![X0,X1,X2,X3]: (X0=join(X0,join(meet(X1,meet(X0,X2)),meet(X0,X3))))),
% 14.50/2.46 inference(forward_demodulation,[status(thm)],[f372,f2391])).
% 14.50/2.46 fof(f2429,plain,(
% 14.50/2.46 ![X0,X1]: (X0=join(meet(X0,X1),X0))),
% 14.50/2.46 inference(forward_demodulation,[status(thm)],[f2389,f2428])).
% 14.50/2.46 fof(f3315,plain,(
% 14.50/2.46 ![X0,X1,X2]: (meet(join(X0,meet(X1,X2)),join(X0,X1))=join(X0,meet(X1,X2)))),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f2429,f108])).
% 14.50/2.46 fof(f3524,plain,(
% 14.50/2.46 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(join(X0,X2),meet(join(X1,meet(X0,X2)),join(X1,X0)))))),
% 14.50/2.46 inference(paramodulation,[status(thm)],[f72,f119])).
% 14.50/2.46 fof(f3652,plain,(
% 14.50/2.46 ~meet(a,join(b,c))=meet(a,meet(join(b,c),join(b,a)))),
% 14.50/2.46 inference(backward_demodulation,[status(thm)],[f3653,f206])).
% 14.50/2.46 fof(f3653,plain,(
% 14.50/2.46 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(join(X0,X2),join(X1,meet(X0,X2)))))),
% 14.50/2.46 inference(forward_demodulation,[status(thm)],[f3315,f3524])).
% 14.50/2.46 fof(f3952,plain,(
% 14.50/2.46 ~meet(a,join(b,c))=meet(join(b,c),a)),
% 14.50/2.46 inference(forward_demodulation,[status(thm)],[f466,f3652])).
% 14.50/2.46 fof(f3953,plain,(
% 14.50/2.46 $false),
% 14.50/2.46 inference(forward_subsumption_resolution,[status(thm)],[f3952,f15])).
% 14.50/2.46 % SZS output end CNFRefutation for theBenchmark.p
% 16.35/3.67 % Elapsed time: 2.980050 seconds
% 16.35/3.67 % CPU time: 7.216301 seconds
% 16.35/3.67 % Total memory used: 46.239 MB
% 16.35/3.67 % Net memory used: 45.421 MB
%------------------------------------------------------------------------------