%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL196-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% 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 : Mon Sep 7 12:42:09 PM UTC 2026
% Result : Unsatisfiable 17.36s 17.67s
% Output : CNFRefutation 17.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 9
% Syntax : Number of clauses : 75 ( 40 unt; 0 nHn; 34 RR)
% Number of literals : 121 ( 0 equ; 47 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 178 ( 26 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_1_2,axiom,
axiom(or(not(or(A,A)),A)) ).
cnf(axiom_1_3,axiom,
axiom(or(not(A),or(B,A))) ).
cnf(axiom_1_4,axiom,
axiom(or(not(or(A,B)),or(B,A))) ).
cnf(axiom_1_5,axiom,
axiom(or(not(or(A,or(B,C))),or(B,or(A,C)))) ).
cnf(axiom_1_6,axiom,
axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B)))) ).
cnf(rule_1,axiom,
( theorem(X)
| ~ axiom(X) ) ).
cnf(rule_2,axiom,
( theorem(X)
| ~ axiom(or(not(Y),X))
| ~ theorem(Y) ) ).
cnf(rule_3,axiom,
( theorem(or(not(X),Z))
| ~ axiom(or(not(X),Y))
| ~ theorem(or(not(Y),Z)) ) ).
cnf(prove_this,negated_conjecture,
~ theorem(or(not(or(p,or(p,q))),or(p,q))) ).
cnf(refute_0_0,plain,
( ~ axiom(or(not(or(A,B)),or(B,A)))
| ~ theorem(or(not(or(B,A)),X_392))
| theorem(or(not(or(A,B)),X_392)) ),
inference(subst,[],[rule_3:[bind(X,$fot(or(A,B))),bind(Y,$fot(or(B,A))),bind(Z,$fot(X_392))]]) ).
cnf(refute_0_1,plain,
( ~ theorem(or(not(or(B,A)),X_392))
| theorem(or(not(or(A,B)),X_392)) ),
inference(resolve,[$cnf( axiom(or(not(or(A,B)),or(B,A))) )],[axiom_1_4,refute_0_0]) ).
cnf(refute_0_2,plain,
( ~ theorem(or(not(or(or(X_35553,X_35554),X_35553)),or(X_35553,X_35554)))
| theorem(or(not(or(X_35553,or(X_35553,X_35554))),or(X_35553,X_35554))) ),
inference(subst,[],[refute_0_1:[bind(A,$fot(X_35553)),bind(B,$fot(or(X_35553,X_35554))),bind(X_392,$fot(or(X_35553,X_35554)))]]) ).
cnf(refute_0_3,plain,
axiom(or(not(X_390),or(B,X_390))),
inference(subst,[],[axiom_1_3:[bind(A,$fot(X_390))]]) ).
cnf(refute_0_4,plain,
( ~ axiom(or(not(X_390),or(B,X_390)))
| ~ theorem(or(not(or(B,X_390)),X_392))
| theorem(or(not(X_390),X_392)) ),
inference(subst,[],[rule_3:[bind(X,$fot(X_390)),bind(Y,$fot(or(B,X_390))),bind(Z,$fot(X_392))]]) ).
cnf(refute_0_5,plain,
( ~ theorem(or(not(or(B,X_390)),X_392))
| theorem(or(not(X_390),X_392)) ),
inference(resolve,[$cnf( axiom(or(not(X_390),or(B,X_390))) )],[refute_0_3,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ theorem(or(not(or(X_35541,or(or(X_35541,X_35542),X_35541))),or(X_35541,X_35542)))
| theorem(or(not(or(or(X_35541,X_35542),X_35541)),or(X_35541,X_35542))) ),
inference(subst,[],[refute_0_5:[bind(B,$fot(X_35541)),bind(X_390,$fot(or(or(X_35541,X_35542),X_35541))),bind(X_392,$fot(or(X_35541,X_35542)))]]) ).
cnf(refute_0_7,plain,
( ~ theorem(or(not(or(or(or(X_32567,X_32568),X_32567),X_32567)),or(X_32567,X_32568)))
| theorem(or(not(or(X_32567,or(or(X_32567,X_32568),X_32567))),or(X_32567,X_32568))) ),
inference(subst,[],[refute_0_1:[bind(A,$fot(X_32567)),bind(B,$fot(or(or(X_32567,X_32568),X_32567))),bind(X_392,$fot(or(X_32567,X_32568)))]]) ).
cnf(refute_0_8,plain,
axiom(or(not(or(X_23,X_23)),X_23)),
inference(subst,[],[axiom_1_2:[bind(A,$fot(X_23))]]) ).
cnf(refute_0_9,plain,
( ~ axiom(or(not(or(X_23,X_23)),X_23))
| ~ theorem(or(X_23,X_23))
| theorem(X_23) ),
inference(subst,[],[rule_2:[bind(X,$fot(X_23)),bind(Y,$fot(or(X_23,X_23)))]]) ).
cnf(refute_0_10,plain,
( ~ theorem(or(X_23,X_23))
| theorem(X_23) ),
inference(resolve,[$cnf( axiom(or(not(or(X_23,X_23)),X_23)) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
( ~ theorem(or(or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562)),or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562))))
| theorem(or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562))) ),
inference(subst,[],[refute_0_10:[bind(X_23,$fot(or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562))))]]) ).
cnf(refute_0_12,plain,
( ~ axiom(or(not(or(A,or(B,C))),or(B,or(A,C))))
| ~ theorem(or(A,or(B,C)))
| theorem(or(B,or(A,C))) ),
inference(subst,[],[rule_2:[bind(X,$fot(or(B,or(A,C)))),bind(Y,$fot(or(A,or(B,C))))]]) ).
cnf(refute_0_13,plain,
( ~ theorem(or(A,or(B,C)))
| theorem(or(B,or(A,C))) ),
inference(resolve,[$cnf( axiom(or(not(or(A,or(B,C))),or(B,or(A,C)))) )],[axiom_1_5,refute_0_12]) ).
cnf(refute_0_14,plain,
( ~ theorem(or(X_32555,or(or(not(or(or(X_32556,X_32557),X_32557)),or(X_32557,X_32558)),X_32556)))
| theorem(or(or(not(or(or(X_32556,X_32557),X_32557)),or(X_32557,X_32558)),or(X_32555,X_32556))) ),
inference(subst,[],[refute_0_13:[bind(A,$fot(X_32555)),bind(B,$fot(or(not(or(or(X_32556,X_32557),X_32557)),or(X_32557,X_32558)))),bind(C,$fot(X_32556))]]) ).
cnf(refute_0_15,plain,
axiom(or(not(X_24),or(B,X_24))),
inference(subst,[],[axiom_1_3:[bind(A,$fot(X_24))]]) ).
cnf(refute_0_16,plain,
( ~ axiom(or(not(X_24),or(B,X_24)))
| ~ theorem(X_24)
| theorem(or(B,X_24)) ),
inference(subst,[],[rule_2:[bind(X,$fot(or(B,X_24))),bind(Y,$fot(X_24))]]) ).
cnf(refute_0_17,plain,
( ~ theorem(X_24)
| theorem(or(B,X_24)) ),
inference(resolve,[$cnf( axiom(or(not(X_24),or(B,X_24))) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
( ~ theorem(or(or(not(or(or(X_32552,X_32553),X_32553)),or(X_32553,X_32554)),X_32552))
| theorem(or(B,or(or(not(or(or(X_32552,X_32553),X_32553)),or(X_32553,X_32554)),X_32552))) ),
inference(subst,[],[refute_0_17:[bind(X_24,$fot(or(or(not(or(or(X_32552,X_32553),X_32553)),or(X_32553,X_32554)),X_32552)))]]) ).
cnf(refute_0_19,plain,
( ~ axiom(or(not(or(A,B)),or(B,A)))
| ~ theorem(or(A,B))
| theorem(or(B,A)) ),
inference(subst,[],[rule_2:[bind(X,$fot(or(B,A))),bind(Y,$fot(or(A,B)))]]) ).
cnf(refute_0_20,plain,
( ~ theorem(or(A,B))
| theorem(or(B,A)) ),
inference(resolve,[$cnf( axiom(or(not(or(A,B)),or(B,A))) )],[axiom_1_4,refute_0_19]) ).
cnf(refute_0_21,plain,
( ~ theorem(or(X_32549,or(not(or(or(X_32549,X_32550),X_32550)),or(X_32550,X_32551))))
| theorem(or(or(not(or(or(X_32549,X_32550),X_32550)),or(X_32550,X_32551)),X_32549)) ),
inference(subst,[],[refute_0_20:[bind(A,$fot(X_32549)),bind(B,$fot(or(not(or(or(X_32549,X_32550),X_32550)),or(X_32550,X_32551))))]]) ).
cnf(refute_0_22,plain,
( ~ theorem(or(not(or(or(X_27350,X_27351),X_27351)),or(X_27350,or(X_27351,X_27352))))
| theorem(or(X_27350,or(not(or(or(X_27350,X_27351),X_27351)),or(X_27351,X_27352)))) ),
inference(subst,[],[refute_0_13:[bind(A,$fot(not(or(or(X_27350,X_27351),X_27351)))),bind(B,$fot(X_27350)),bind(C,$fot(or(X_27351,X_27352)))]]) ).
cnf(refute_0_23,plain,
( ~ theorem(or(not(or(X_26559,or(X_26558,X_26559))),or(X_26558,or(X_26559,X_26560))))
| theorem(or(not(or(or(X_26558,X_26559),X_26559)),or(X_26558,or(X_26559,X_26560)))) ),
inference(subst,[],[refute_0_1:[bind(A,$fot(or(X_26558,X_26559))),bind(B,$fot(X_26559)),bind(X_392,$fot(or(X_26558,or(X_26559,X_26560))))]]) ).
cnf(refute_0_24,plain,
( ~ axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B))))
| ~ theorem(or(not(A),B))
| theorem(or(not(or(C,A)),or(C,B))) ),
inference(subst,[],[rule_2:[bind(X,$fot(or(not(or(C,A)),or(C,B)))),bind(Y,$fot(or(not(A),B)))]]) ).
cnf(refute_0_25,plain,
( ~ theorem(or(not(A),B))
| theorem(or(not(or(C,A)),or(C,B))) ),
inference(resolve,[$cnf( axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B)))) )],[axiom_1_6,refute_0_24]) ).
cnf(refute_0_26,plain,
( ~ theorem(or(not(or(X_981,X_981)),or(X_981,X_980)))
| theorem(or(not(or(C,or(X_981,X_981))),or(C,or(X_981,X_980)))) ),
inference(subst,[],[refute_0_25:[bind(A,$fot(or(X_981,X_981))),bind(B,$fot(or(X_981,X_980)))]]) ).
cnf(refute_0_27,plain,
axiom(or(not(or(X_391,X_391)),X_391)),
inference(subst,[],[axiom_1_2:[bind(A,$fot(X_391))]]) ).
cnf(refute_0_28,plain,
( ~ axiom(or(not(or(X_391,X_391)),X_391))
| ~ theorem(or(not(X_391),X_392))
| theorem(or(not(or(X_391,X_391)),X_392)) ),
inference(subst,[],[rule_3:[bind(X,$fot(or(X_391,X_391))),bind(Y,$fot(X_391)),bind(Z,$fot(X_392))]]) ).
cnf(refute_0_29,plain,
( ~ theorem(or(not(X_391),X_392))
| theorem(or(not(or(X_391,X_391)),X_392)) ),
inference(resolve,[$cnf( axiom(or(not(or(X_391,X_391)),X_391)) )],[refute_0_27,refute_0_28]) ).
cnf(refute_0_30,plain,
( ~ theorem(or(not(X_964),or(X_964,X_963)))
| theorem(or(not(or(X_964,X_964)),or(X_964,X_963))) ),
inference(subst,[],[refute_0_29:[bind(X_391,$fot(X_964)),bind(X_392,$fot(or(X_964,X_963)))]]) ).
cnf(refute_0_31,plain,
( ~ axiom(or(not(or(X_7,X_8)),or(X_8,X_7)))
| theorem(or(not(or(X_7,X_8)),or(X_8,X_7))) ),
inference(subst,[],[rule_1:[bind(X,$fot(or(not(or(X_7,X_8)),or(X_8,X_7))))]]) ).
cnf(refute_0_32,plain,
axiom(or(not(or(X_7,X_8)),or(X_8,X_7))),
inference(subst,[],[axiom_1_4:[bind(A,$fot(X_7)),bind(B,$fot(X_8))]]) ).
cnf(refute_0_33,plain,
theorem(or(not(or(X_7,X_8)),or(X_8,X_7))),
inference(resolve,[$cnf( axiom(or(not(or(X_7,X_8)),or(X_8,X_7))) )],[refute_0_32,refute_0_31]) ).
cnf(refute_0_34,plain,
theorem(or(not(or(X_958,X_959)),or(X_959,X_958))),
inference(subst,[],[refute_0_33:[bind(X_7,$fot(X_958)),bind(X_8,$fot(X_959))]]) ).
cnf(refute_0_35,plain,
( ~ theorem(or(not(or(X_958,X_959)),or(X_959,X_958)))
| theorem(or(not(X_959),or(X_959,X_958))) ),
inference(subst,[],[refute_0_5:[bind(B,$fot(X_958)),bind(X_390,$fot(X_959)),bind(X_392,$fot(or(X_959,X_958)))]]) ).
cnf(refute_0_36,plain,
theorem(or(not(X_959),or(X_959,X_958))),
inference(resolve,[$cnf( theorem(or(not(or(X_958,X_959)),or(X_959,X_958))) )],[refute_0_34,refute_0_35]) ).
cnf(refute_0_37,plain,
theorem(or(not(X_964),or(X_964,X_963))),
inference(subst,[],[refute_0_36:[bind(X_958,$fot(X_963)),bind(X_959,$fot(X_964))]]) ).
cnf(refute_0_38,plain,
theorem(or(not(or(X_964,X_964)),or(X_964,X_963))),
inference(resolve,[$cnf( theorem(or(not(X_964),or(X_964,X_963))) )],[refute_0_37,refute_0_30]) ).
cnf(refute_0_39,plain,
theorem(or(not(or(X_981,X_981)),or(X_981,X_980))),
inference(subst,[],[refute_0_38:[bind(X_963,$fot(X_980)),bind(X_964,$fot(X_981))]]) ).
cnf(refute_0_40,plain,
theorem(or(not(or(C,or(X_981,X_981))),or(C,or(X_981,X_980)))),
inference(resolve,[$cnf( theorem(or(not(or(X_981,X_981)),or(X_981,X_980))) )],[refute_0_39,refute_0_26]) ).
cnf(refute_0_41,plain,
theorem(or(not(or(X_25953,or(X_25954,X_25954))),or(X_25953,or(X_25954,X_980)))),
inference(subst,[],[refute_0_40:[bind(C,$fot(X_25953)),bind(X_981,$fot(X_25954))]]) ).
cnf(refute_0_42,plain,
( ~ axiom(or(not(or(A,or(B,C))),or(B,or(A,C))))
| ~ theorem(or(not(or(B,or(A,C))),X_392))
| theorem(or(not(or(A,or(B,C))),X_392)) ),
inference(subst,[],[rule_3:[bind(X,$fot(or(A,or(B,C)))),bind(Y,$fot(or(B,or(A,C)))),bind(Z,$fot(X_392))]]) ).
cnf(refute_0_43,plain,
( ~ theorem(or(not(or(B,or(A,C))),X_392))
| theorem(or(not(or(A,or(B,C))),X_392)) ),
inference(resolve,[$cnf( axiom(or(not(or(A,or(B,C))),or(B,or(A,C)))) )],[axiom_1_5,refute_0_42]) ).
cnf(refute_0_44,plain,
( ~ theorem(or(not(or(X_25953,or(X_25954,X_25954))),or(X_25953,or(X_25954,X_980))))
| theorem(or(not(or(X_25954,or(X_25953,X_25954))),or(X_25953,or(X_25954,X_980)))) ),
inference(subst,[],[refute_0_43:[bind(A,$fot(X_25954)),bind(B,$fot(X_25953)),bind(C,$fot(X_25954)),bind(X_392,$fot(or(X_25953,or(X_25954,X_980))))]]) ).
cnf(refute_0_45,plain,
theorem(or(not(or(X_25954,or(X_25953,X_25954))),or(X_25953,or(X_25954,X_980)))),
inference(resolve,[$cnf( theorem(or(not(or(X_25953,or(X_25954,X_25954))),or(X_25953,or(X_25954,X_980)))) )],[refute_0_41,refute_0_44]) ).
cnf(refute_0_46,plain,
theorem(or(not(or(X_26559,or(X_26558,X_26559))),or(X_26558,or(X_26559,X_26560)))),
inference(subst,[],[refute_0_45:[bind(X_25953,$fot(X_26558)),bind(X_25954,$fot(X_26559)),bind(X_980,$fot(X_26560))]]) ).
cnf(refute_0_47,plain,
theorem(or(not(or(or(X_26558,X_26559),X_26559)),or(X_26558,or(X_26559,X_26560)))),
inference(resolve,[$cnf( theorem(or(not(or(X_26559,or(X_26558,X_26559))),or(X_26558,or(X_26559,X_26560)))) )],[refute_0_46,refute_0_23]) ).
cnf(refute_0_48,plain,
theorem(or(not(or(or(X_27350,X_27351),X_27351)),or(X_27350,or(X_27351,X_27352)))),
inference(subst,[],[refute_0_47:[bind(X_26558,$fot(X_27350)),bind(X_26559,$fot(X_27351)),bind(X_26560,$fot(X_27352))]]) ).
cnf(refute_0_49,plain,
theorem(or(X_27350,or(not(or(or(X_27350,X_27351),X_27351)),or(X_27351,X_27352)))),
inference(resolve,[$cnf( theorem(or(not(or(or(X_27350,X_27351),X_27351)),or(X_27350,or(X_27351,X_27352)))) )],[refute_0_48,refute_0_22]) ).
cnf(refute_0_50,plain,
theorem(or(X_32549,or(not(or(or(X_32549,X_32550),X_32550)),or(X_32550,X_32551)))),
inference(subst,[],[refute_0_49:[bind(X_27350,$fot(X_32549)),bind(X_27351,$fot(X_32550)),bind(X_27352,$fot(X_32551))]]) ).
cnf(refute_0_51,plain,
theorem(or(or(not(or(or(X_32549,X_32550),X_32550)),or(X_32550,X_32551)),X_32549)),
inference(resolve,[$cnf( theorem(or(X_32549,or(not(or(or(X_32549,X_32550),X_32550)),or(X_32550,X_32551)))) )],[refute_0_50,refute_0_21]) ).
cnf(refute_0_52,plain,
theorem(or(or(not(or(or(X_32552,X_32553),X_32553)),or(X_32553,X_32554)),X_32552)),
inference(subst,[],[refute_0_51:[bind(X_32549,$fot(X_32552)),bind(X_32550,$fot(X_32553)),bind(X_32551,$fot(X_32554))]]) ).
cnf(refute_0_53,plain,
theorem(or(B,or(or(not(or(or(X_32552,X_32553),X_32553)),or(X_32553,X_32554)),X_32552))),
inference(resolve,[$cnf( theorem(or(or(not(or(or(X_32552,X_32553),X_32553)),or(X_32553,X_32554)),X_32552)) )],[refute_0_52,refute_0_18]) ).
cnf(refute_0_54,plain,
theorem(or(X_32555,or(or(not(or(or(X_32556,X_32557),X_32557)),or(X_32557,X_32558)),X_32556))),
inference(subst,[],[refute_0_53:[bind(B,$fot(X_32555)),bind(X_32552,$fot(X_32556)),bind(X_32553,$fot(X_32557)),bind(X_32554,$fot(X_32558))]]) ).
cnf(refute_0_55,plain,
theorem(or(or(not(or(or(X_32556,X_32557),X_32557)),or(X_32557,X_32558)),or(X_32555,X_32556))),
inference(resolve,[$cnf( theorem(or(X_32555,or(or(not(or(or(X_32556,X_32557),X_32557)),or(X_32557,X_32558)),X_32556))) )],[refute_0_54,refute_0_14]) ).
cnf(refute_0_56,plain,
theorem(or(or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562)),or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562)))),
inference(subst,[],[refute_0_55:[bind(X_32555,$fot(not(or(or(or(X_32561,X_32562),X_32561),X_32561)))),bind(X_32556,$fot(or(X_32561,X_32562))),bind(X_32557,$fot(X_32561)),bind(X_32558,$fot(X_32562))]]) ).
cnf(refute_0_57,plain,
theorem(or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562))),
inference(resolve,[$cnf( theorem(or(or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562)),or(not(or(or(or(X_32561,X_32562),X_32561),X_32561)),or(X_32561,X_32562)))) )],[refute_0_56,refute_0_11]) ).
cnf(refute_0_58,plain,
theorem(or(not(or(or(or(X_32567,X_32568),X_32567),X_32567)),or(X_32567,X_32568))),
inference(subst,[],[refute_0_57:[bind(X_32561,$fot(X_32567)),bind(X_32562,$fot(X_32568))]]) ).
cnf(refute_0_59,plain,
theorem(or(not(or(X_32567,or(or(X_32567,X_32568),X_32567))),or(X_32567,X_32568))),
inference(resolve,[$cnf( theorem(or(not(or(or(or(X_32567,X_32568),X_32567),X_32567)),or(X_32567,X_32568))) )],[refute_0_58,refute_0_7]) ).
cnf(refute_0_60,plain,
theorem(or(not(or(X_35541,or(or(X_35541,X_35542),X_35541))),or(X_35541,X_35542))),
inference(subst,[],[refute_0_59:[bind(X_32567,$fot(X_35541)),bind(X_32568,$fot(X_35542))]]) ).
cnf(refute_0_61,plain,
theorem(or(not(or(or(X_35541,X_35542),X_35541)),or(X_35541,X_35542))),
inference(resolve,[$cnf( theorem(or(not(or(X_35541,or(or(X_35541,X_35542),X_35541))),or(X_35541,X_35542))) )],[refute_0_60,refute_0_6]) ).
cnf(refute_0_62,plain,
theorem(or(not(or(or(X_35553,X_35554),X_35553)),or(X_35553,X_35554))),
inference(subst,[],[refute_0_61:[bind(X_35541,$fot(X_35553)),bind(X_35542,$fot(X_35554))]]) ).
cnf(refute_0_63,plain,
theorem(or(not(or(X_35553,or(X_35553,X_35554))),or(X_35553,X_35554))),
inference(resolve,[$cnf( theorem(or(not(or(or(X_35553,X_35554),X_35553)),or(X_35553,X_35554))) )],[refute_0_62,refute_0_2]) ).
cnf(refute_0_64,plain,
theorem(or(not(or(p,or(p,q))),or(p,q))),
inference(subst,[],[refute_0_63:[bind(X_35553,$fot(p)),bind(X_35554,$fot(q))]]) ).
cnf(refute_0_65,plain,
$false,
inference(resolve,[$cnf( theorem(or(not(or(p,or(p,q))),or(p,q))) )],[refute_0_64,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL196-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.02 % Command : metis --show proof --show saturation %s
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Sat Sep 5 04:09:57 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 17.36/17.67 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.36/17.67
% 17.36/17.67 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 17.36/17.68
%------------------------------------------------------------------------------