Anne is big. Anne is kind. Anne is nice. Anne is quiet. Anne is rough. Anne is round. Anne is young. If Anne is young and Anne is nice then Anne is big. If something is nice and big then it is rough. If something is quiet and big then it is nice. If something is rough then it is round. All quiet, round things are kind. Quiet things are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is young and Anne is nice then Anne is big.
((("Anne" "is" "young" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
If something is nice and big then it is rough.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and big then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
All quiet, round things are kind.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Anne is nice.
True
1
proof
[(triple3 OR ((triple4 triple1) -> rule3))]
("Anne" "is" "nice" "+")
triple3
((triple4 triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple3 OR ((triple4 triple1) -> rule3))]
("Anne" "is" "nice" "-")
triple3
((triple4 triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
@0: Anne is big.[(triple1 OR ((triple7 triple3) -> rule1))] Anne is kind.[(triple2 OR ((triple4 triple6) -> rule5) OR ((triple4 ((triple4) -> rule6)) -> rule5) OR ((triple4 ((triple5) -> rule4)) -> rule5) OR ((triple4 ((((triple3 triple1) -> rule2)) -> rule4)) -> rule5) OR ((triple4 ((((triple3 ((triple7 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule5) OR ((triple4 ((((((triple4 triple1) -> rule3) triple1) -> rule2)) -> rule4)) -> rule5) OR ((triple4 ((((((triple4 triple1) -> rule3) ((triple7 triple3) -> rule1)) -> rule2)) -> rule4)) -> rule5))] Anne is nice.[(triple3 OR ((triple4 triple1) -> rule3))] Anne is quiet.[(triple4)] Anne is rough.[(triple5 OR ((triple3 triple1) -> rule2) OR ((triple3 ((triple7 triple3) -> rule1)) -> rule2) OR ((((triple4 triple1) -> rule3) triple1) -> rule2) OR ((((triple4 triple1) -> rule3) ((triple7 triple3) -> rule1)) -> rule2))] Anne is round.[(triple6 OR ((triple4) -> rule6) OR ((triple5) -> rule4) OR ((((triple3 triple1) -> rule2)) -> rule4) OR ((((triple3 ((triple7 triple3) -> rule1)) -> rule2)) -> rule4) OR ((((((triple4 triple1) -> rule3) triple1) -> rule2)) -> rule4) OR ((((((triple4 triple1) -> rule3) ((triple7 triple3) -> rule1)) -> rule2)) -> rule4))] Anne is young.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple7 triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4 triple6) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple4 ((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((triple4 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((triple4 ((((triple3 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
((triple4 ((((triple3 ((triple7 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((triple4 ((((((triple4 triple1) -> (rule3 % int4)) triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((triple4 ((((((triple4 triple1) -> (rule3 % int5)) ((triple7 triple3) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple4 triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple3 triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple3 ((triple7 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple4 triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple4 triple1) -> (rule3 % int3)) ((triple7 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple4) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple5) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple3 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple3 ((triple7 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple4 triple1) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((triple4 triple1) -> (rule3 % int4)) ((triple7 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
triple7