%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP114-1 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 07:27:22 AM UTC 2026
% Result : Unsatisfiable 88.84s 12.72s
% Output : CNFRefutation 88.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 73
% Number of leaves : 21
% Syntax : Number of formulae : 205 ( 205 unt; 0 def)
% Number of atoms : 205 ( 204 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 68 ( 68 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 352 ( 12 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(inverse_of_identity,axiom,
inverse(identity) = identity,
file('theBenchmark.p',inverse_of_identity) ).
cnf(c_4,plain,
inverse(identity) = identity,
inference(clausify,[status(thm)],[inverse_of_identity]) ).
fof(inverse_involution,axiom,
! [VAR_0] : inverse(inverse(VAR_0)) = VAR_0,
file('theBenchmark.p',inverse_involution) ).
cnf(c_5,plain,
inverse(inverse(A)) = A,
inference(clausify,[status(thm)],[inverse_involution]) ).
fof(inverse_product_lemma,axiom,
! [VAR_0,VAR_1] : inverse(multiply(VAR_0,VAR_1)) = multiply(inverse(VAR_1),inverse(VAR_0)),
file('theBenchmark.p',inverse_product_lemma) ).
cnf(c_6,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(clausify,[status(thm)],[inverse_product_lemma]) ).
fof(intersection_idempotent,axiom,
! [VAR_0] : intersection(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',intersection_idempotent) ).
cnf(c_7,plain,
intersection(A,A) = A,
inference(clausify,[status(thm)],[intersection_idempotent]) ).
fof(union_idempotent,axiom,
! [VAR_0] : union(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',union_idempotent) ).
cnf(c_8,plain,
union(A,A) = A,
inference(clausify,[status(thm)],[union_idempotent]) ).
fof(intersection_commutative,axiom,
! [VAR_0,VAR_1] : intersection(VAR_0,VAR_1) = intersection(VAR_1,VAR_0),
file('theBenchmark.p',intersection_commutative) ).
cnf(c_9,plain,
intersection(A,B) = intersection(B,A),
inference(clausify,[status(thm)],[intersection_commutative]) ).
fof(union_commutative,axiom,
! [VAR_0,VAR_1] : union(VAR_0,VAR_1) = union(VAR_1,VAR_0),
file('theBenchmark.p',union_commutative) ).
cnf(c_10,plain,
union(A,B) = union(B,A),
inference(clausify,[status(thm)],[union_commutative]) ).
fof(intersection_associative,axiom,
! [VAR_0,VAR_1,VAR_2] : intersection(VAR_0,intersection(VAR_1,VAR_2)) = intersection(intersection(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',intersection_associative) ).
cnf(c_11,plain,
intersection(A,intersection(B,C)) = intersection(intersection(A,B),C),
inference(clausify,[status(thm)],[intersection_associative]) ).
cnf(c_12,plain,
intersection(intersection(A,B),C) = intersection(A,intersection(B,C)),
inference(copy,[status(thm)],[c_11]) ).
fof(union_associative,axiom,
! [VAR_0,VAR_1,VAR_2] : union(VAR_0,union(VAR_1,VAR_2)) = union(union(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',union_associative) ).
cnf(c_13,plain,
union(A,union(B,C)) = union(union(A,B),C),
inference(clausify,[status(thm)],[union_associative]) ).
cnf(c_14,plain,
union(union(A,B),C) = union(A,union(B,C)),
inference(copy,[status(thm)],[c_13]) ).
fof(union_intersection_absorbtion,axiom,
! [VAR_0,VAR_1] : union(intersection(VAR_0,VAR_1),VAR_1) = VAR_1,
file('theBenchmark.p',union_intersection_absorbtion) ).
cnf(c_15,plain,
union(intersection(A,B),B) = B,
inference(clausify,[status(thm)],[union_intersection_absorbtion]) ).
cnf(c_16,plain,
union(A,intersection(B,A)) = A,
inference(paramod,[status(thm)],[c_10,c_15]) ).
fof(intersection_union_absorbtion,axiom,
! [VAR_0,VAR_1] : intersection(union(VAR_0,VAR_1),VAR_1) = VAR_1,
file('theBenchmark.p',intersection_union_absorbtion) ).
cnf(c_17,plain,
intersection(union(A,B),B) = B,
inference(clausify,[status(thm)],[intersection_union_absorbtion]) ).
cnf(c_18,plain,
intersection(A,union(B,A)) = A,
inference(paramod,[status(thm)],[c_9,c_17]) ).
fof(multiply_union1,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,union(VAR_1,VAR_2)) = union(multiply(VAR_0,VAR_1),multiply(VAR_0,VAR_2)),
file('theBenchmark.p',multiply_union1) ).
cnf(c_19,plain,
multiply(A,union(B,C)) = union(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[multiply_union1]) ).
cnf(c_20,plain,
union(multiply(A,B),multiply(A,C)) = multiply(A,union(B,C)),
inference(copy,[status(thm)],[c_19]) ).
fof(multiply_intersection1,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,intersection(VAR_1,VAR_2)) = intersection(multiply(VAR_0,VAR_1),multiply(VAR_0,VAR_2)),
file('theBenchmark.p',multiply_intersection1) ).
cnf(c_21,plain,
multiply(A,intersection(B,C)) = intersection(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[multiply_intersection1]) ).
cnf(c_22,plain,
intersection(multiply(A,B),multiply(A,C)) = multiply(A,intersection(B,C)),
inference(copy,[status(thm)],[c_21]) ).
fof(multiply_union2,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(union(VAR_0,VAR_1),VAR_2) = union(multiply(VAR_0,VAR_2),multiply(VAR_1,VAR_2)),
file('theBenchmark.p',multiply_union2) ).
cnf(c_23,plain,
multiply(union(A,B),C) = union(multiply(A,C),multiply(B,C)),
inference(clausify,[status(thm)],[multiply_union2]) ).
cnf(c_24,plain,
union(multiply(A,B),multiply(C,B)) = multiply(union(A,C),B),
inference(copy,[status(thm)],[c_23]) ).
fof(multiply_intersection2,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(intersection(VAR_0,VAR_1),VAR_2) = intersection(multiply(VAR_0,VAR_2),multiply(VAR_1,VAR_2)),
file('theBenchmark.p',multiply_intersection2) ).
cnf(c_25,plain,
multiply(intersection(A,B),C) = intersection(multiply(A,C),multiply(B,C)),
inference(clausify,[status(thm)],[multiply_intersection2]) ).
cnf(c_26,plain,
intersection(multiply(A,B),multiply(C,B)) = multiply(intersection(A,C),B),
inference(copy,[status(thm)],[c_25]) ).
fof(positive_part,axiom,
! [VAR_0] : positive_part(VAR_0) = union(VAR_0,identity),
file('theBenchmark.p',positive_part) ).
cnf(c_27,plain,
positive_part(A) = union(A,identity),
inference(clausify,[status(thm)],[positive_part]) ).
fof(negative_part,axiom,
! [VAR_0] : negative_part(VAR_0) = intersection(VAR_0,identity),
file('theBenchmark.p',negative_part) ).
cnf(c_28,plain,
negative_part(A) = intersection(A,identity),
inference(clausify,[status(thm)],[negative_part]) ).
fof(prove_product,axiom,
multiply(positive_part(a),negative_part(a)) != a,
file('theBenchmark.p',prove_product) ).
cnf(c_29,plain,
multiply(positive_part(a),negative_part(a)) != a,
inference(clausify,[status(thm)],[prove_product]) ).
cnf(c_7684,plain,
multiply(union(a,identity),negative_part(a)) != a,
inference(paramod,[status(thm)],[c_27,c_29]) ).
cnf(c_7685,plain,
multiply(union(identity,a),negative_part(a)) != a,
inference(paramod,[status(thm)],[c_10,c_7684]) ).
cnf(c_7686,plain,
multiply(union(identity,a),intersection(a,identity)) != a,
inference(paramod,[status(thm)],[c_28,c_7685]) ).
cnf(c_30,plain,
multiply(union(identity,a),intersection(identity,a)) != a,
inference(paramod,[status(thm)],[c_9,c_7686]) ).
cnf(c_7687,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_7688,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_7687]) ).
cnf(c_31,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_7688]) ).
cnf(c_32,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_7689,plain,
inverse(A) = multiply(inverse(A),inverse(identity)),
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_7690,plain,
inverse(A) = multiply(inverse(A),identity),
inference(paramod,[status(thm)],[c_4,c_7689]) ).
cnf(c_33,plain,
multiply(inverse(A),identity) = inverse(A),
inference(copy,[status(thm)],[c_7690]) ).
cnf(c_7691,plain,
intersection(A,B) = intersection(A,intersection(A,B)),
inference(paramod,[status(thm)],[c_7,c_12]) ).
cnf(c_35,plain,
intersection(A,intersection(A,B)) = intersection(A,B),
inference(copy,[status(thm)],[c_7691]) ).
cnf(c_7692,plain,
union(A,B) = union(A,union(A,B)),
inference(paramod,[status(thm)],[c_8,c_14]) ).
cnf(c_40,plain,
union(A,union(A,B)) = union(A,B),
inference(copy,[status(thm)],[c_7692]) ).
cnf(c_7693,plain,
union(union(A,B),B) = union(A,B),
inference(paramod,[status(thm)],[c_8,c_14]) ).
cnf(c_41,plain,
union(A,union(B,A)) = union(B,A),
inference(paramod,[status(thm)],[c_10,c_7693]) ).
cnf(c_44,plain,
union(A,intersection(A,B)) = A,
inference(paramod,[status(thm)],[c_9,c_16]) ).
cnf(c_7694,plain,
union(A,B) = union(A,union(intersection(C,A),B)),
inference(paramod,[status(thm)],[c_16,c_14]) ).
cnf(c_46,plain,
union(A,union(intersection(B,A),C)) = union(A,C),
inference(copy,[status(thm)],[c_7694]) ).
cnf(c_48,plain,
intersection(A,union(A,B)) = A,
inference(paramod,[status(thm)],[c_10,c_18]) ).
cnf(c_7695,plain,
intersection(A,B) = intersection(A,intersection(union(C,A),B)),
inference(paramod,[status(thm)],[c_18,c_12]) ).
cnf(c_49,plain,
intersection(A,intersection(union(B,A),C)) = intersection(A,C),
inference(copy,[status(thm)],[c_7695]) ).
cnf(c_55,plain,
intersection(identity,multiply(inverse(A),B)) = multiply(inverse(A),intersection(A,B)),
inference(paramod,[status(thm)],[c_2,c_22]) ).
cnf(c_58,plain,
union(A,multiply(B,A)) = multiply(union(identity,B),A),
inference(paramod,[status(thm)],[c_1,c_24]) ).
cnf(c_65,plain,
intersection(A,multiply(B,A)) = multiply(intersection(identity,B),A),
inference(paramod,[status(thm)],[c_1,c_26]) ).
cnf(c_7696,plain,
intersection(multiply(A,B),identity) = multiply(intersection(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_2,c_26]) ).
cnf(c_68,plain,
intersection(identity,multiply(A,B)) = multiply(intersection(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_9,c_7696]) ).
cnf(c_7697,plain,
multiply(identity,A) = multiply(B,multiply(inverse(B),A)),
inference(paramod,[status(thm)],[c_32,c_3]) ).
cnf(c_7698,plain,
A = multiply(B,multiply(inverse(B),A)),
inference(paramod,[status(thm)],[c_1,c_7697]) ).
cnf(c_72,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(copy,[status(thm)],[c_7698]) ).
cnf(c_79,plain,
intersection(identity,multiply(A,inverse(B))) = multiply(intersection(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_32,c_26]) ).
cnf(c_7699,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_5,c_33]) ).
cnf(c_81,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_5,c_7699]) ).
cnf(c_84,plain,
union(A,multiply(A,B)) = multiply(A,union(identity,B)),
inference(paramod,[status(thm)],[c_81,c_20]) ).
cnf(c_86,plain,
intersection(A,multiply(A,B)) = multiply(A,intersection(identity,B)),
inference(paramod,[status(thm)],[c_81,c_22]) ).
cnf(c_7700,plain,
intersection(inverse(A),identity) = multiply(intersection(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_32,c_65]) ).
cnf(c_162,plain,
intersection(identity,inverse(A)) = multiply(intersection(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_9,c_7700]) ).
cnf(c_7701,plain,
multiply(inverse(A),union(A,multiply(A,B))) = union(identity,B),
inference(paramod,[status(thm)],[c_84,c_31]) ).
cnf(c_196,plain,
union(identity,A) = multiply(inverse(B),union(B,multiply(B,A))),
inference(copy,[status(thm)],[c_7701]) ).
cnf(c_7702,plain,
multiply(A,union(identity,A)) = multiply(union(identity,A),A),
inference(paramod,[status(thm)],[c_84,c_58]) ).
cnf(c_200,plain,
multiply(union(identity,A),A) = multiply(A,union(identity,A)),
inference(copy,[status(thm)],[c_7702]) ).
cnf(c_7703,plain,
intersection(inverse(A),identity) = multiply(inverse(A),intersection(identity,A)),
inference(paramod,[status(thm)],[c_2,c_86]) ).
cnf(c_7704,plain,
intersection(identity,inverse(A)) = multiply(inverse(A),intersection(identity,A)),
inference(paramod,[status(thm)],[c_9,c_7703]) ).
cnf(c_229,plain,
multiply(intersection(identity,A),inverse(A)) = multiply(inverse(A),intersection(identity,A)),
inference(paramod,[status(thm)],[c_162,c_7704]) ).
cnf(c_7705,plain,
intersection(union(identity,a),multiply(union(identity,a),a)) != a,
inference(paramod,[status(thm)],[c_86,c_30]) ).
cnf(c_7706,plain,
intersection(union(identity,a),multiply(a,union(identity,a))) != a,
inference(paramod,[status(thm)],[c_200,c_7705]) ).
cnf(c_243,plain,
multiply(intersection(identity,a),union(identity,a)) != a,
inference(paramod,[status(thm)],[c_65,c_7706]) ).
cnf(c_7707,plain,
multiply(inverse(A),intersection(A,multiply(A,B))) = intersection(identity,B),
inference(paramod,[status(thm)],[c_86,c_31]) ).
cnf(c_244,plain,
intersection(identity,A) = multiply(inverse(B),intersection(B,multiply(B,A))),
inference(copy,[status(thm)],[c_7707]) ).
cnf(c_245,plain,
intersection(inverse(A),B) = multiply(inverse(A),intersection(identity,multiply(A,B))),
inference(paramod,[status(thm)],[c_31,c_86]) ).
cnf(c_246,plain,
intersection(A,multiply(A,intersection(identity,B))) = intersection(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_86,c_35]) ).
cnf(c_7708,plain,
multiply(A,intersection(identity,A)) = multiply(intersection(identity,A),A),
inference(paramod,[status(thm)],[c_86,c_65]) ).
cnf(c_251,plain,
multiply(intersection(identity,A),A) = multiply(A,intersection(identity,A)),
inference(copy,[status(thm)],[c_7708]) ).
cnf(c_256,plain,
intersection(identity,inverse(A)) = multiply(inverse(A),intersection(identity,A)),
inference(paramod,[status(thm)],[c_229,c_162]) ).
cnf(c_7709,plain,
multiply(multiply(A,intersection(identity,A)),B) = multiply(intersection(identity,A),multiply(A,B)),
inference(paramod,[status(thm)],[c_251,c_3]) ).
cnf(c_7710,plain,
multiply(A,multiply(intersection(identity,A),B)) = multiply(intersection(identity,A),multiply(A,B)),
inference(paramod,[status(thm)],[c_3,c_7709]) ).
cnf(c_299,plain,
multiply(intersection(identity,A),multiply(A,B)) = multiply(A,multiply(intersection(identity,A),B)),
inference(copy,[status(thm)],[c_7710]) ).
cnf(c_7711,plain,
inverse(multiply(inverse(A),intersection(identity,A))) = multiply(inverse(inverse(A)),inverse(intersection(identity,A))),
inference(paramod,[status(thm)],[c_229,c_6]) ).
cnf(c_7712,plain,
multiply(inverse(intersection(identity,A)),inverse(inverse(A))) = multiply(inverse(inverse(A)),inverse(intersection(identity,A))),
inference(paramod,[status(thm)],[c_6,c_7711]) ).
cnf(c_7713,plain,
multiply(inverse(intersection(identity,A)),A) = multiply(inverse(inverse(A)),inverse(intersection(identity,A))),
inference(paramod,[status(thm)],[c_5,c_7712]) ).
cnf(c_333,plain,
multiply(inverse(intersection(identity,A)),A) = multiply(A,inverse(intersection(identity,A))),
inference(paramod,[status(thm)],[c_5,c_7713]) ).
cnf(c_481,plain,
union(multiply(A,B),C) = multiply(A,union(B,multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_72,c_20]) ).
cnf(c_482,plain,
intersection(multiply(A,B),C) = multiply(A,intersection(B,multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_72,c_22]) ).
cnf(c_978,plain,
multiply(intersection(identity,a),multiply(inverse(A),union(A,multiply(A,a)))) != a,
inference(paramod,[status(thm)],[c_196,c_243]) ).
cnf(c_1034,plain,
multiply(intersection(identity,a),multiply(inverse(union(A,B)),union(A,union(B,multiply(union(A,B),a))))) != a,
inference(paramod,[status(thm)],[c_14,c_978]) ).
cnf(c_7714,plain,
multiply(intersection(identity,a),multiply(inverse(union(A,B)),union(B,union(union(A,B),multiply(union(B,union(A,B)),a))))) != a,
inference(paramod,[status(thm)],[c_41,c_1034]) ).
cnf(c_7715,plain,
multiply(intersection(identity,a),multiply(inverse(union(A,B)),union(B,union(union(A,B),multiply(union(A,B),a))))) != a,
inference(paramod,[status(thm)],[c_41,c_7714]) ).
cnf(c_1053,plain,
multiply(intersection(identity,a),multiply(inverse(union(A,B)),union(B,multiply(union(A,B),union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_84,c_7715]) ).
cnf(c_7716,plain,
intersection(union(intersection(A,B),C),union(B,C)) = union(intersection(A,B),C),
inference(paramod,[status(thm)],[c_46,c_18]) ).
cnf(c_1168,plain,
intersection(union(A,B),union(intersection(C,A),B)) = union(intersection(C,A),B),
inference(paramod,[status(thm)],[c_9,c_7716]) ).
cnf(c_1176,plain,
union(A,multiply(intersection(B,A),union(identity,C))) = union(A,multiply(intersection(B,A),C)),
inference(paramod,[status(thm)],[c_84,c_46]) ).
cnf(c_1493,plain,
intersection(A,multiply(intersection(identity,B),union(C,A))) = intersection(A,multiply(B,union(C,A))),
inference(paramod,[status(thm)],[c_65,c_49]) ).
cnf(c_7717,plain,
multiply(intersection(identity,a),multiply(inverse(A),union(intersection(B,A),multiply(union(A,intersection(B,A)),union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_16,c_1053]) ).
cnf(c_1695,plain,
multiply(intersection(identity,a),multiply(inverse(A),union(intersection(B,A),multiply(A,union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_16,c_7717]) ).
cnf(c_1739,plain,
union(intersection(A,intersection(identity,a)),multiply(intersection(identity,a),union(identity,a))) != a,
inference(paramod,[status(thm)],[c_72,c_1695]) ).
cnf(c_7718,plain,
union(multiply(inverse(A),intersection(A,multiply(A,intersection(identity,a)))),multiply(intersection(identity,a),union(identity,a))) != a,
inference(paramod,[status(thm)],[c_244,c_1739]) ).
cnf(c_7719,plain,
union(multiply(inverse(A),intersection(A,multiply(A,a))),multiply(intersection(identity,a),union(identity,a))) != a,
inference(paramod,[status(thm)],[c_246,c_7718]) ).
cnf(c_7720,plain,
multiply(inverse(A),union(intersection(A,multiply(A,a)),multiply(inverse(inverse(A)),multiply(intersection(identity,a),union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_481,c_7719]) ).
cnf(c_1756,plain,
multiply(inverse(A),union(intersection(A,multiply(A,a)),multiply(A,multiply(intersection(identity,a),union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_5,c_7720]) ).
cnf(c_7721,plain,
intersection(identity,multiply(multiply(A,B),inverse(A))) = multiply(multiply(A,intersection(identity,B)),inverse(A)),
inference(paramod,[status(thm)],[c_86,c_79]) ).
cnf(c_7722,plain,
intersection(identity,multiply(A,multiply(B,inverse(A)))) = multiply(multiply(A,intersection(identity,B)),inverse(A)),
inference(paramod,[status(thm)],[c_3,c_7721]) ).
cnf(c_2616,plain,
intersection(identity,multiply(A,multiply(B,inverse(A)))) = multiply(A,multiply(intersection(identity,B),inverse(A))),
inference(paramod,[status(thm)],[c_3,c_7722]) ).
cnf(c_7723,plain,
intersection(union(multiply(A,B),C),union(multiply(intersection(A,inverse(B)),B),C)) = union(intersection(identity,multiply(A,B)),C),
inference(paramod,[status(thm)],[c_68,c_1168]) ).
cnf(c_7724,plain,
intersection(multiply(A,union(B,multiply(inverse(A),C))),union(multiply(intersection(A,inverse(B)),B),C)) = union(intersection(identity,multiply(A,B)),C),
inference(paramod,[status(thm)],[c_481,c_7723]) ).
cnf(c_7725,plain,
intersection(multiply(A,union(B,multiply(inverse(A),C))),multiply(intersection(A,inverse(B)),union(B,multiply(inverse(intersection(A,inverse(B))),C)))) = union(intersection(identity,multiply(A,B)),C),
inference(paramod,[status(thm)],[c_481,c_7724]) ).
cnf(c_7726,plain,
multiply(A,intersection(union(B,multiply(inverse(A),C)),multiply(inverse(A),multiply(intersection(A,inverse(B)),union(B,multiply(inverse(intersection(A,inverse(B))),C)))))) = union(intersection(identity,multiply(A,B)),C),
inference(paramod,[status(thm)],[c_482,c_7725]) ).
cnf(c_7475,plain,
union(intersection(identity,multiply(A,B)),C) = multiply(A,intersection(union(B,multiply(inverse(A),C)),multiply(inverse(A),multiply(intersection(A,inverse(B)),union(B,multiply(inverse(intersection(A,inverse(B))),C)))))),
inference(copy,[status(thm)],[c_7726]) ).
cnf(c_7727,plain,
intersection(union(multiply(inverse(A),B),C),union(multiply(inverse(A),intersection(A,B)),C)) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_55,c_1168]) ).
cnf(c_7728,plain,
intersection(multiply(inverse(A),union(B,multiply(inverse(inverse(A)),C))),union(multiply(inverse(A),intersection(A,B)),C)) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_481,c_7727]) ).
cnf(c_7729,plain,
intersection(multiply(inverse(A),union(B,multiply(A,C))),union(multiply(inverse(A),intersection(A,B)),C)) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_5,c_7728]) ).
cnf(c_7730,plain,
intersection(multiply(inverse(A),union(B,multiply(A,C))),multiply(inverse(A),union(intersection(A,B),multiply(inverse(inverse(A)),C)))) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_481,c_7729]) ).
cnf(c_7731,plain,
intersection(multiply(inverse(A),union(B,multiply(A,C))),multiply(inverse(A),union(intersection(A,B),multiply(A,C)))) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_5,c_7730]) ).
cnf(c_7732,plain,
multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(inverse(inverse(A)),multiply(inverse(A),union(intersection(A,B),multiply(A,C)))))) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_482,c_7731]) ).
cnf(c_7733,plain,
multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(inverse(A),union(intersection(A,B),multiply(A,C)))))) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_5,c_7732]) ).
cnf(c_7734,plain,
multiply(inverse(A),intersection(union(B,multiply(A,C)),union(intersection(A,B),multiply(A,C)))) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_72,c_7733]) ).
cnf(c_7735,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = union(intersection(identity,multiply(inverse(A),B)),C),
inference(paramod,[status(thm)],[c_1168,c_7734]) ).
cnf(c_7736,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(inverse(inverse(A)),C)),multiply(inverse(inverse(A)),multiply(intersection(inverse(A),inverse(B)),union(B,multiply(inverse(intersection(inverse(A),inverse(B))),C)))))),
inference(paramod,[status(thm)],[c_7475,c_7735]) ).
cnf(c_7737,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(inverse(inverse(A)),multiply(intersection(inverse(A),inverse(B)),union(B,multiply(inverse(intersection(inverse(A),inverse(B))),C)))))),
inference(paramod,[status(thm)],[c_5,c_7736]) ).
cnf(c_7738,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(intersection(inverse(A),inverse(B)),union(B,multiply(inverse(intersection(inverse(A),inverse(B))),C)))))),
inference(paramod,[status(thm)],[c_5,c_7737]) ).
cnf(c_7739,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(multiply(inverse(A),intersection(identity,multiply(A,inverse(B)))),union(B,multiply(inverse(intersection(inverse(A),inverse(B))),C)))))),
inference(paramod,[status(thm)],[c_245,c_7738]) ).
cnf(c_7740,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(multiply(inverse(A),intersection(identity,multiply(A,inverse(B)))),union(B,multiply(inverse(multiply(inverse(A),intersection(identity,multiply(A,inverse(B))))),C)))))),
inference(paramod,[status(thm)],[c_245,c_7739]) ).
cnf(c_7741,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(multiply(inverse(A),intersection(identity,multiply(A,inverse(B)))),union(B,multiply(multiply(inverse(intersection(identity,multiply(A,inverse(B)))),inverse(inverse(A))),C)))))),
inference(paramod,[status(thm)],[c_6,c_7740]) ).
cnf(c_7742,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(multiply(inverse(A),intersection(identity,multiply(A,inverse(B)))),union(B,multiply(multiply(inverse(intersection(identity,multiply(A,inverse(B)))),A),C)))))),
inference(paramod,[status(thm)],[c_5,c_7741]) ).
cnf(c_7743,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(multiply(inverse(A),intersection(identity,multiply(A,inverse(B)))),union(B,multiply(inverse(intersection(identity,multiply(A,inverse(B)))),multiply(A,C))))))),
inference(paramod,[status(thm)],[c_3,c_7742]) ).
cnf(c_7744,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(A,multiply(inverse(A),multiply(intersection(identity,multiply(A,inverse(B))),union(B,multiply(inverse(intersection(identity,multiply(A,inverse(B)))),multiply(A,C)))))))),
inference(paramod,[status(thm)],[c_3,c_7743]) ).
cnf(c_7517,plain,
multiply(inverse(A),union(intersection(A,B),multiply(A,C))) = multiply(inverse(A),intersection(union(B,multiply(A,C)),multiply(intersection(identity,multiply(A,inverse(B))),union(B,multiply(inverse(intersection(identity,multiply(A,inverse(B)))),multiply(A,C)))))),
inference(paramod,[status(thm)],[c_72,c_7744]) ).
cnf(c_7745,plain,
multiply(inverse(A),intersection(union(multiply(A,a),multiply(A,multiply(intersection(identity,a),union(identity,a)))),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_7517,c_1756]) ).
cnf(c_7746,plain,
multiply(inverse(A),intersection(multiply(A,union(a,multiply(inverse(A),multiply(A,multiply(intersection(identity,a),union(identity,a)))))),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_481,c_7745]) ).
cnf(c_7747,plain,
multiply(inverse(A),intersection(multiply(A,union(a,multiply(intersection(identity,a),union(identity,a)))),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_31,c_7746]) ).
cnf(c_7748,plain,
multiply(inverse(A),intersection(multiply(A,union(a,multiply(intersection(identity,a),a))),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_1176,c_7747]) ).
cnf(c_7749,plain,
multiply(inverse(A),intersection(multiply(A,union(a,multiply(a,intersection(identity,a)))),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_251,c_7748]) ).
cnf(c_7750,plain,
multiply(inverse(A),intersection(multiply(A,multiply(a,union(identity,intersection(identity,a)))),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_84,c_7749]) ).
cnf(c_7751,plain,
multiply(inverse(A),intersection(multiply(A,multiply(a,identity)),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_44,c_7750]) ).
cnf(c_7752,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(intersection(identity,multiply(A,inverse(multiply(A,a)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_81,c_7751]) ).
cnf(c_7753,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(intersection(identity,multiply(A,multiply(inverse(a),inverse(A)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_6,c_7752]) ).
cnf(c_7754,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(intersection(identity,inverse(a)),inverse(A))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_2616,c_7753]) ).
cnf(c_7755,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(multiply(inverse(a),intersection(identity,a)),inverse(A))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_256,c_7754]) ).
cnf(c_7756,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,inverse(multiply(A,a))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7755]) ).
cnf(c_7757,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(inverse(intersection(identity,multiply(A,multiply(inverse(a),inverse(A))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_6,c_7756]) ).
cnf(c_7758,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(inverse(multiply(A,multiply(intersection(identity,inverse(a)),inverse(A)))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_2616,c_7757]) ).
cnf(c_7759,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(inverse(multiply(A,multiply(multiply(inverse(a),intersection(identity,a)),inverse(A)))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_256,c_7758]) ).
cnf(c_7760,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(inverse(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A))))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7759]) ).
cnf(c_7761,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(inverse(multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_6,c_7760]) ).
cnf(c_7762,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(multiply(inverse(multiply(intersection(identity,a),inverse(A))),inverse(inverse(a))),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_6,c_7761]) ).
cnf(c_7763,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(multiply(multiply(inverse(inverse(A)),inverse(intersection(identity,a))),inverse(inverse(a))),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_6,c_7762]) ).
cnf(c_7764,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(multiply(multiply(A,inverse(intersection(identity,a))),inverse(inverse(a))),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_5,c_7763]) ).
cnf(c_7765,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(multiply(multiply(A,inverse(intersection(identity,a))),a),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_5,c_7764]) ).
cnf(c_7766,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(multiply(A,multiply(inverse(intersection(identity,a)),a)),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7765]) ).
cnf(c_7767,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(multiply(A,multiply(a,inverse(intersection(identity,a)))),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_333,c_7766]) ).
cnf(c_7768,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(A,multiply(multiply(a,inverse(intersection(identity,a))),inverse(A))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7767]) ).
cnf(c_7769,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(multiply(A,multiply(a,multiply(inverse(intersection(identity,a)),inverse(A)))),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7768]) ).
cnf(c_7770,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(A,multiply(multiply(a,multiply(inverse(intersection(identity,a)),inverse(A))),multiply(A,multiply(intersection(identity,a),union(identity,a))))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7769]) ).
cnf(c_7771,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(A,multiply(a,multiply(multiply(inverse(intersection(identity,a)),inverse(A)),multiply(A,multiply(intersection(identity,a),union(identity,a)))))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7770]) ).
cnf(c_7772,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(A,multiply(a,multiply(inverse(intersection(identity,a)),multiply(inverse(A),multiply(A,multiply(intersection(identity,a),union(identity,a))))))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7771]) ).
cnf(c_7773,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(A,multiply(a,multiply(inverse(intersection(identity,a)),multiply(intersection(identity,a),union(identity,a))))))))) != a,
inference(paramod,[status(thm)],[c_31,c_7772]) ).
cnf(c_7774,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),union(multiply(A,a),multiply(A,multiply(a,union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_31,c_7773]) ).
cnf(c_7775,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),multiply(A,union(a,multiply(inverse(A),multiply(A,multiply(a,union(identity,a))))))))) != a,
inference(paramod,[status(thm)],[c_481,c_7774]) ).
cnf(c_7776,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),multiply(A,union(a,multiply(a,union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_31,c_7775]) ).
cnf(c_7777,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),multiply(A,multiply(a,union(identity,union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_84,c_7776]) ).
cnf(c_7778,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(multiply(A,multiply(inverse(a),multiply(intersection(identity,a),inverse(A)))),multiply(A,multiply(a,union(identity,a)))))) != a,
inference(paramod,[status(thm)],[c_40,c_7777]) ).
cnf(c_7779,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(A,multiply(multiply(inverse(a),multiply(intersection(identity,a),inverse(A))),multiply(A,multiply(a,union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7778]) ).
cnf(c_7780,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(A,multiply(inverse(a),multiply(multiply(intersection(identity,a),inverse(A)),multiply(A,multiply(a,union(identity,a)))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7779]) ).
cnf(c_7781,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(A,multiply(inverse(a),multiply(intersection(identity,a),multiply(inverse(A),multiply(A,multiply(a,union(identity,a))))))))) != a,
inference(paramod,[status(thm)],[c_3,c_7780]) ).
cnf(c_7782,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(A,multiply(inverse(a),multiply(intersection(identity,a),multiply(a,union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_31,c_7781]) ).
cnf(c_7783,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(A,multiply(inverse(a),multiply(a,multiply(intersection(identity,a),union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_299,c_7782]) ).
cnf(c_7784,plain,
multiply(inverse(A),intersection(multiply(A,a),multiply(A,multiply(intersection(identity,a),union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_31,c_7783]) ).
cnf(c_7785,plain,
multiply(inverse(A),multiply(A,intersection(a,multiply(inverse(A),multiply(A,multiply(intersection(identity,a),union(identity,a))))))) != a,
inference(paramod,[status(thm)],[c_482,c_7784]) ).
cnf(c_7786,plain,
multiply(inverse(A),multiply(A,intersection(a,multiply(intersection(identity,a),union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_31,c_7785]) ).
cnf(c_7787,plain,
multiply(inverse(A),multiply(A,intersection(a,multiply(a,union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_1493,c_7786]) ).
cnf(c_7788,plain,
multiply(inverse(A),multiply(A,multiply(a,intersection(identity,union(identity,a))))) != a,
inference(paramod,[status(thm)],[c_86,c_7787]) ).
cnf(c_7789,plain,
multiply(inverse(A),multiply(A,multiply(a,identity))) != a,
inference(paramod,[status(thm)],[c_48,c_7788]) ).
cnf(c_7790,plain,
multiply(inverse(A),multiply(A,a)) != a,
inference(paramod,[status(thm)],[c_81,c_7789]) ).
cnf(c_7791,plain,
a != a,
inference(paramod,[status(thm)],[c_31,c_7790]) ).
cnf(c_7683,plain,
$false,
inference(copy,[status(thm)],[c_7791]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP114-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n014.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 14:22:48 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 417432 was started by sandbox on n014,
% 0.17/0.45 % Fri Sep 25 14:22:48 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 88.84/12.72
% 88.84/12.72 % SZS status Unsatisfiable for theBenchmark
% 88.84/12.72
% 88.84/12.72 % Proof 1 at 3.29 (+ 0.86) seconds.
% 88.84/12.72 % Length of proof is 76.
% 88.84/12.72 % Level of proof is 12.
% 88.84/12.72 % Maximum clause weight is 92.000.
% 88.84/12.72 % Given clauses 312.
% 88.84/12.72
% 88.84/12.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------