Anne is big. Anne is furry. Anne is red. Anne is rough. Anne is round. Bob is cold. Bob is furry. Bob is red. Bob is round. Bob is young. If someone is red then they are cold. Cold people are furry. Furry, cold people are red. If Bob is cold then Bob is rough. If someone is rough and young then they are big. Young people are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Furry, cold people are red.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Bob is cold then Bob is rough.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "rough" "+"))
If someone is rough and young then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple2 OR ((((triple3) -> rule1)) -> rule2))]
("Anne" "is" "furry" "+")
triple2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is not furry.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule2) OR ((((triple8) -> rule1)) -> rule2) OR ((((((triple10) -> rule6)) -> rule1)) -> rule2))]
("Bob" "is" "furry" "-")
triple7
((triple6) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Anne is cold.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple6) -> rule4) OR ((((triple8) -> rule1)) -> rule4) OR ((((((triple10) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "rough" "-")
((triple6) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is big.
True
4
proof
[(((((triple6) -> rule4) triple10) -> rule5) OR ((((((triple8) -> rule1)) -> rule4) triple10) -> rule5) OR ((((((((triple10) -> rule6)) -> rule1)) -> rule4) triple10) -> rule5))]
("Bob" "is" "big" "+")
((((triple6) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is not big.
False
4
inv-proof
[(((((triple6) -> rule4) triple10) -> rule5) OR ((((((triple8) -> rule1)) -> rule4) triple10) -> rule5) OR ((((((((triple10) -> rule6)) -> rule1)) -> rule4) triple10) -> rule5))]
("Bob" "is" "big" "-")
((((triple6) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((((triple3) -> rule1)) -> rule2))] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5)] Bob is cold.[(triple6 OR ((triple8) -> rule1) OR ((((triple10) -> rule6)) -> rule1))] Bob is furry.[(triple7 OR ((triple6) -> rule2) OR ((((triple8) -> rule1)) -> rule2) OR ((((((triple10) -> rule6)) -> rule1)) -> rule2))] Bob is red.[(triple8 OR ((triple10) -> rule6) OR ((triple7 triple6) -> rule3) OR ((((triple6) -> rule2) triple6) -> rule3))] Bob is round.[(triple9)] Bob is young.[(triple10)] @1: Anne is cold.[(((triple3) -> rule1))] Bob is rough.[(((triple6) -> rule4) OR ((((triple8) -> rule1)) -> rule4) OR ((((((triple10) -> rule6)) -> rule1)) -> rule4))] @2: Bob is big.[(((((triple6) -> rule4) triple10) -> rule5) OR ((((((triple8) -> rule1)) -> rule4) triple10) -> rule5) OR ((((((((triple10) -> rule6)) -> rule1)) -> rule4) triple10) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Bob is cold.
("Bob" "is" "cold" "+")
triple6
((triple8) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple7
((triple6) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple8
((triple10) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple7 triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple9
Bob is young.
("Bob" "is" "young" "+")
triple10
Anne is cold.
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple6) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((triple6) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4