%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWV251-2 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 20:30:40 EDT 2022
% Result : Unsatisfiable 14.21s 14.44s
% Output : CNFRefutation 14.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 18
% Syntax : Number of clauses : 63 ( 34 unt; 0 nHn; 33 RR)
% Number of literals : 102 ( 36 equ; 40 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 118 ( 21 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_Message_Oanalz__mono_0,axiom,
( ~ c_lessequals(V_G,V_H,tc_set(tc_Message_Omsg))
| c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg)) ) ).
cnf(cls_Set_OUn__Diff__cancel_0,axiom,
c_union(V_A,c_minus(V_B,V_A,tc_set(T_a)),T_a) = c_union(V_A,V_B,T_a) ).
cnf(cls_Set_OUn__subset__iff_0,axiom,
( ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))
| c_lessequals(V_A,V_C,tc_set(T_a)) ) ).
cnf(cls_Set_OUn__subset__iff_1,axiom,
( ~ c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a))
| c_lessequals(V_B,V_C,tc_set(T_a)) ) ).
cnf(cls_Set_OUn__subset__iff_2,axiom,
( ~ c_lessequals(V_B,V_C,tc_set(T_a))
| ~ c_lessequals(V_A,V_C,tc_set(T_a))
| c_lessequals(c_union(V_A,V_B,T_a),V_C,tc_set(T_a)) ) ).
cnf(cls_Set_Oinsert__Diff1_0,axiom,
( ~ c_in(V_x,V_B,T_a)
| c_minus(c_insert(V_x,V_A,T_a),V_B,tc_set(T_a)) = c_minus(V_A,V_B,tc_set(T_a)) ) ).
cnf(cls_Set_OsubsetD_0,axiom,
( ~ c_in(V_c,V_A,T_a)
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(V_c,V_B,T_a) ) ).
cnf(cls_Set_Osubset__antisym_0,axiom,
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| V_A = V_B ) ).
cnf(cls_Set_Osubset__refl_0,axiom,
c_lessequals(V_A,V_A,tc_set(T_a)) ).
cnf(cls_conjecture_0,negated_conjecture,
c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg) ).
cnf(cls_conjecture_1,negated_conjecture,
c_in(v_x,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg) ).
cnf(cls_conjecture_2,negated_conjecture,
~ c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg) ).
cnf(refute_0_0,plain,
( ~ c_lessequals(X_204,c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg),tc_set(tc_Message_Omsg))
| c_lessequals(c_Message_Oanalz(X_204),c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)),tc_set(tc_Message_Omsg)) ),
inference(subst,[],[cls_Message_Oanalz__mono_0:[bind(V_G,$fot(X_204)),bind(V_H,$fot(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)))]]) ).
cnf(refute_0_1,plain,
c_lessequals(c_union(X_77,X_78,X_76),c_union(X_77,X_78,X_76),tc_set(X_76)),
inference(subst,[],[cls_Set_Osubset__refl_0:[bind(T_a,$fot(X_76)),bind(V_A,$fot(c_union(X_77,X_78,X_76)))]]) ).
cnf(refute_0_2,plain,
( ~ c_lessequals(c_union(X_77,X_78,X_76),c_union(X_77,X_78,X_76),tc_set(X_76))
| c_lessequals(X_77,c_union(X_77,X_78,X_76),tc_set(X_76)) ),
inference(subst,[],[cls_Set_OUn__subset__iff_0:[bind(T_a,$fot(X_76)),bind(V_A,$fot(X_77)),bind(V_B,$fot(X_78)),bind(V_C,$fot(c_union(X_77,X_78,X_76)))]]) ).
cnf(refute_0_3,plain,
c_lessequals(X_77,c_union(X_77,X_78,X_76),tc_set(X_76)),
inference(resolve,[$cnf( c_lessequals(c_union(X_77,X_78,X_76),c_union(X_77,X_78,X_76),tc_set(X_76)) )],[refute_0_1,refute_0_2]) ).
cnf(refute_0_4,plain,
c_lessequals(c_union(X_174,X_175,X_173),c_union(c_union(X_174,X_175,X_173),X_78,X_173),tc_set(X_173)),
inference(subst,[],[refute_0_3:[bind(X_76,$fot(X_173)),bind(X_77,$fot(c_union(X_174,X_175,X_173)))]]) ).
cnf(refute_0_5,plain,
( ~ c_lessequals(c_union(X_174,X_175,X_173),c_union(c_union(X_174,X_175,X_173),X_78,X_173),tc_set(X_173))
| c_lessequals(X_175,c_union(c_union(X_174,X_175,X_173),X_78,X_173),tc_set(X_173)) ),
inference(subst,[],[cls_Set_OUn__subset__iff_1:[bind(T_a,$fot(X_173)),bind(V_A,$fot(X_174)),bind(V_B,$fot(X_175)),bind(V_C,$fot(c_union(c_union(X_174,X_175,X_173),X_78,X_173)))]]) ).
cnf(refute_0_6,plain,
c_lessequals(X_175,c_union(c_union(X_174,X_175,X_173),X_78,X_173),tc_set(X_173)),
inference(resolve,[$cnf( c_lessequals(c_union(X_174,X_175,X_173),c_union(c_union(X_174,X_175,X_173),X_78,X_173),tc_set(X_173)) )],[refute_0_4,refute_0_5]) ).
cnf(refute_0_7,plain,
c_lessequals(X_204,c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg),tc_set(tc_Message_Omsg)),
inference(subst,[],[refute_0_6:[bind(X_173,$fot(tc_Message_Omsg)),bind(X_174,$fot(X_203)),bind(X_175,$fot(X_204)),bind(X_78,$fot(X_205))]]) ).
cnf(refute_0_8,plain,
c_lessequals(c_Message_Oanalz(X_204),c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)),tc_set(tc_Message_Omsg)),
inference(resolve,[$cnf( c_lessequals(X_204,c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg),tc_set(tc_Message_Omsg)) )],[refute_0_7,refute_0_0]) ).
cnf(refute_0_9,plain,
( ~ c_in(X_1813,c_Message_Oanalz(X_204),tc_Message_Omsg)
| ~ c_lessequals(c_Message_Oanalz(X_204),c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)),tc_set(tc_Message_Omsg))
| c_in(X_1813,c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)),tc_Message_Omsg) ),
inference(subst,[],[cls_Set_OsubsetD_0:[bind(T_a,$fot(tc_Message_Omsg)),bind(V_A,$fot(c_Message_Oanalz(X_204))),bind(V_B,$fot(c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)))),bind(V_c,$fot(X_1813))]]) ).
cnf(refute_0_10,plain,
( ~ c_in(X_1813,c_Message_Oanalz(X_204),tc_Message_Omsg)
| c_in(X_1813,c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)),tc_Message_Omsg) ),
inference(resolve,[$cnf( c_lessequals(c_Message_Oanalz(X_204),c_Message_Oanalz(c_union(c_union(X_203,X_204,tc_Message_Omsg),X_205,tc_Message_Omsg)),tc_set(tc_Message_Omsg)) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
( ~ c_in(v_x,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6539,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),X_6541,tc_Message_Omsg)),tc_Message_Omsg) ),
inference(subst,[],[refute_0_10:[bind(X_1813,$fot(v_x)),bind(X_203,$fot(X_6539)),bind(X_204,$fot(c_insert(v_X,v_H,tc_Message_Omsg))),bind(X_205,$fot(X_6541))]]) ).
cnf(refute_0_12,plain,
c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6539,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),X_6541,tc_Message_Omsg)),tc_Message_Omsg),
inference(resolve,[$cnf( c_in(v_x,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg) )],[cls_conjecture_1,refute_0_11]) ).
cnf(refute_0_13,plain,
c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),
inference(subst,[],[refute_0_12:[bind(X_6539,$fot(X_6542)),bind(X_6541,$fot(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)))]]) ).
cnf(refute_0_14,plain,
c_lessequals(X_12,X_12,tc_set(X_10)),
inference(subst,[],[cls_Set_Osubset__refl_0:[bind(T_a,$fot(X_10)),bind(V_A,$fot(X_12))]]) ).
cnf(refute_0_15,plain,
( ~ c_lessequals(X_12,X_12,tc_set(X_10))
| c_lessequals(c_union(X_12,X_12,X_10),X_12,tc_set(X_10)) ),
inference(subst,[],[cls_Set_OUn__subset__iff_2:[bind(T_a,$fot(X_10)),bind(V_A,$fot(X_12)),bind(V_B,$fot(X_12)),bind(V_C,$fot(X_12))]]) ).
cnf(refute_0_16,plain,
c_lessequals(c_union(X_12,X_12,X_10),X_12,tc_set(X_10)),
inference(resolve,[$cnf( c_lessequals(X_12,X_12,tc_set(X_10)) )],[refute_0_14,refute_0_15]) ).
cnf(refute_0_17,plain,
c_lessequals(c_union(X_491,X_491,X_489),X_491,tc_set(X_489)),
inference(subst,[],[refute_0_16:[bind(X_10,$fot(X_489)),bind(X_12,$fot(X_491))]]) ).
cnf(refute_0_18,plain,
( ~ c_lessequals(X_491,c_union(X_491,X_491,X_489),tc_set(X_489))
| ~ c_lessequals(c_union(X_491,X_491,X_489),X_491,tc_set(X_489))
| c_union(X_491,X_491,X_489) = X_491 ),
inference(subst,[],[cls_Set_Osubset__antisym_0:[bind(T_a,$fot(X_489)),bind(V_A,$fot(c_union(X_491,X_491,X_489))),bind(V_B,$fot(X_491))]]) ).
cnf(refute_0_19,plain,
( ~ c_lessequals(X_491,c_union(X_491,X_491,X_489),tc_set(X_489))
| c_union(X_491,X_491,X_489) = X_491 ),
inference(resolve,[$cnf( c_lessequals(c_union(X_491,X_491,X_489),X_491,tc_set(X_489)) )],[refute_0_17,refute_0_18]) ).
cnf(refute_0_20,plain,
c_lessequals(c_union(X_174,X_175,X_173),c_union(X_174,X_175,X_173),tc_set(X_173)),
inference(subst,[],[cls_Set_Osubset__refl_0:[bind(T_a,$fot(X_173)),bind(V_A,$fot(c_union(X_174,X_175,X_173)))]]) ).
cnf(refute_0_21,plain,
( ~ c_lessequals(c_union(X_174,X_175,X_173),c_union(X_174,X_175,X_173),tc_set(X_173))
| c_lessequals(X_175,c_union(X_174,X_175,X_173),tc_set(X_173)) ),
inference(subst,[],[cls_Set_OUn__subset__iff_1:[bind(T_a,$fot(X_173)),bind(V_A,$fot(X_174)),bind(V_B,$fot(X_175)),bind(V_C,$fot(c_union(X_174,X_175,X_173)))]]) ).
cnf(refute_0_22,plain,
c_lessequals(X_175,c_union(X_174,X_175,X_173),tc_set(X_173)),
inference(resolve,[$cnf( c_lessequals(c_union(X_174,X_175,X_173),c_union(X_174,X_175,X_173),tc_set(X_173)) )],[refute_0_20,refute_0_21]) ).
cnf(refute_0_23,plain,
c_lessequals(X_491,c_union(X_491,X_491,X_489),tc_set(X_489)),
inference(subst,[],[refute_0_22:[bind(X_173,$fot(X_489)),bind(X_174,$fot(X_491)),bind(X_175,$fot(X_491))]]) ).
cnf(refute_0_24,plain,
c_union(X_491,X_491,X_489) = X_491,
inference(resolve,[$cnf( c_lessequals(X_491,c_union(X_491,X_491,X_489),tc_set(X_489)) )],[refute_0_23,refute_0_19]) ).
cnf(refute_0_25,plain,
c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg) = c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),
inference(subst,[],[refute_0_24:[bind(X_489,$fot(tc_Message_Omsg)),bind(X_491,$fot(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)))]]) ).
cnf(refute_0_26,plain,
( c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg) != c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)
| ~ c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg)
| c_in(v_x,c_Message_Oanalz(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(tautology,[equality,[$cnf( c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) ),[1,0],$fot(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg))]]) ).
cnf(refute_0_27,plain,
( ~ c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg)
| c_in(v_x,c_Message_Oanalz(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) ),
inference(resolve,[$cnf( $equal(c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
c_in(v_x,c_Message_Oanalz(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),
inference(resolve,[$cnf( c_in(v_x,c_Message_Oanalz(c_union(c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(X_6542,c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) )],[refute_0_13,refute_0_27]) ).
cnf(refute_0_29,plain,
c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),
inference(subst,[],[refute_0_28:[bind(X_6542,$fot(c_Message_Osynth(c_Message_Oanalz(v_G))))]]) ).
cnf(refute_0_30,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg),
inference(subst,[],[cls_Set_OUn__Diff__cancel_0:[bind(T_a,$fot(tc_Message_Omsg)),bind(V_A,$fot(c_Message_Osynth(c_Message_Oanalz(v_G)))),bind(V_B,$fot(c_insert(v_X,X_706,tc_Message_Omsg)))]]) ).
cnf(refute_0_31,plain,
( ~ c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)
| c_minus(c_insert(v_X,X_703,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)) = c_minus(X_703,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)) ),
inference(subst,[],[cls_Set_Oinsert__Diff1_0:[bind(T_a,$fot(tc_Message_Omsg)),bind(V_A,$fot(X_703)),bind(V_B,$fot(c_Message_Osynth(c_Message_Oanalz(v_G)))),bind(V_x,$fot(v_X))]]) ).
cnf(refute_0_32,plain,
c_minus(c_insert(v_X,X_703,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)) = c_minus(X_703,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),
inference(resolve,[$cnf( c_in(v_X,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg) )],[cls_conjecture_0,refute_0_31]) ).
cnf(refute_0_33,plain,
c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)) = c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),
inference(subst,[],[refute_0_32:[bind(X_703,$fot(X_706))]]) ).
cnf(refute_0_34,plain,
( c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)) != c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg))
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg) ),
introduced(tautology,[equality,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)) ),[0,1],$fot(c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)))]]) ).
cnf(refute_0_35,plain,
( c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg) ),
inference(resolve,[$cnf( $equal(c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg))) )],[refute_0_33,refute_0_34]) ).
cnf(refute_0_36,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg),
inference(resolve,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(c_insert(v_X,X_706,tc_Message_Omsg),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)) )],[refute_0_30,refute_0_35]) ).
cnf(refute_0_37,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg),
inference(subst,[],[cls_Set_OUn__Diff__cancel_0:[bind(T_a,$fot(tc_Message_Omsg)),bind(V_A,$fot(c_Message_Osynth(c_Message_Oanalz(v_G)))),bind(V_B,$fot(X_706))]]) ).
cnf(refute_0_38,plain,
( c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg)
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg) ),
introduced(tautology,[equality,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)) ),[0],$fot(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg))]]) ).
cnf(refute_0_39,plain,
( c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg) ),
inference(resolve,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg)) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X_706,tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg),
inference(resolve,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_minus(X_706,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_set(tc_Message_Omsg)),tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,X_706,tc_Message_Omsg),tc_Message_Omsg)) )],[refute_0_36,refute_0_39]) ).
cnf(refute_0_41,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),
inference(subst,[],[refute_0_40:[bind(X_706,$fot(v_H))]]) ).
cnf(refute_0_42,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_43,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_44,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
( c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)
| c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg) ),
inference(subst,[],[refute_0_44:[bind(X,$fot(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg))),bind(Y,$fot(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)))]]) ).
cnf(refute_0_46,plain,
c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg) = c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg),
inference(resolve,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)) )],[refute_0_41,refute_0_45]) ).
cnf(refute_0_47,plain,
( c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg) != c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)
| ~ c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg)
| c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg) ),
introduced(tautology,[equality,[$cnf( c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) ),[1,0],$fot(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg))]]) ).
cnf(refute_0_48,plain,
( ~ c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg)
| c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg) ),
inference(resolve,[$cnf( $equal(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg),c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)) )],[refute_0_46,refute_0_47]) ).
cnf(refute_0_49,plain,
c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg),
inference(resolve,[$cnf( c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_insert(v_X,v_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) )],[refute_0_29,refute_0_48]) ).
cnf(refute_0_50,plain,
$false,
inference(resolve,[$cnf( c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg) )],[refute_0_49,cls_conjecture_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SWV251-2 : TPTP v8.1.0. Released v3.2.0.
% 0.08/0.13 % Command : metis --show proof --show saturation %s
% 0.13/0.35 % Computer : n023.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Wed Jun 15 04:12:20 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 14.21/14.44 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.21/14.44
% 14.21/14.44 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 14.21/14.44
%------------------------------------------------------------------------------