Anne is big. Anne is blue. Anne is furry. Anne is kind. Anne is round. Anne is smart. Anne is young. Erin is big. Erin is blue. Erin is furry. Erin is kind. Erin is round. Erin is smart. Erin is young. If someone is young then they are furry. Big people are round. If someone is round and kind then they are blue. Round people are smart. Furry people are kind. All big people are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is round and kind then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Erin is smart.
True
1
proof
[(triple13 OR ((triple12) -> rule4) OR ((((triple8) -> rule2)) -> rule4))]
("Erin" "is" "smart" "+")
triple13
((triple12) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not young.
False
1
inv-proof
[(triple14 OR ((triple8) -> rule6))]
("Erin" "is" "young" "-")
triple14
((triple8) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple5 triple4) -> rule3) OR ((triple5 ((triple3) -> rule5)) -> rule3) OR ((((triple1) -> rule2) triple4) -> rule3) OR ((((triple1) -> rule2) ((triple3) -> rule5)) -> rule3) OR ((triple5 ((((triple7) -> rule1)) -> rule5)) -> rule3) OR ((((triple1) -> rule2) ((((triple7) -> rule1)) -> rule5)) -> rule3) OR ((triple5 ((((((triple1) -> rule6)) -> rule1)) -> rule5)) -> rule3) OR ((((triple1) -> rule2) ((((((triple1) -> rule6)) -> rule1)) -> rule5)) -> rule3))] Anne is furry.[(triple3 OR ((triple7) -> rule1) OR ((((triple1) -> rule6)) -> rule1))] Anne is kind.[(triple4 OR ((triple3) -> rule5) OR ((((triple7) -> rule1)) -> rule5) OR ((((((triple1) -> rule6)) -> rule1)) -> rule5))] Anne is round.[(triple5 OR ((triple1) -> rule2))] Anne is smart.[(triple6 OR ((triple5) -> rule4) OR ((((triple1) -> rule2)) -> rule4))] Anne is young.[(triple7 OR ((triple1) -> rule6))] Erin is big.[(triple8)] Erin is blue.[(triple9 OR ((triple12 triple11) -> rule3) OR ((triple12 ((triple10) -> rule5)) -> rule3) OR ((((triple8) -> rule2) triple11) -> rule3) OR ((((triple8) -> rule2) ((triple10) -> rule5)) -> rule3) OR ((triple12 ((((triple14) -> rule1)) -> rule5)) -> rule3) OR ((((triple8) -> rule2) ((((triple14) -> rule1)) -> rule5)) -> rule3) OR ((triple12 ((((((triple8) -> rule6)) -> rule1)) -> rule5)) -> rule3) OR ((((triple8) -> rule2) ((((((triple8) -> rule6)) -> rule1)) -> rule5)) -> rule3))] Erin is furry.[(triple10 OR ((triple14) -> rule1) OR ((((triple8) -> rule6)) -> rule1))] Erin is kind.[(triple11 OR ((triple10) -> rule5) OR ((((triple14) -> rule1)) -> rule5) OR ((((((triple8) -> rule6)) -> rule1)) -> rule5))] Erin is round.[(triple12 OR ((triple8) -> rule2))] Erin is smart.[(triple13 OR ((triple12) -> rule4) OR ((((triple8) -> rule2)) -> rule4))] Erin is young.[(triple14 OR ((triple8) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple5 triple4) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple5 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple1) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple5 ((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((triple1) -> (rule2 % int4)) ((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((triple5 ((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((((triple1) -> (rule2 % int5)) ((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple7) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple3) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple5) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
((triple12 triple11) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple12 ((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple8) -> (rule2 % int2)) triple11) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple8) -> (rule2 % int3)) ((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple12 ((((triple14) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple8) -> (rule2 % int4)) ((((triple14) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((triple12 ((((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((triple8) -> (rule2 % int5)) ((((((triple8) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Erin is furry.
("Erin" "is" "furry" "+")
triple10
((triple14) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple11
((triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple12
((triple8) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple13
((triple12) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple8) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1