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