Anne is big. Anne is cold. Anne is furry. Anne is green. Anne is red. Anne is rough. Anne is round. Charlie is not cold. Charlie is furry. Charlie is red. Charlie is rough. Charlie is round. All furry things are big. If Charlie is furry and Charlie is green then Charlie is big. Cold things are round. If Charlie is big then Charlie is green. Big things are green. All furry, red things are rough. If something is green and not round then it is rough. Green, cold things are rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Charlie is furry and Charlie is green then Charlie is big.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "big" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If Charlie is big then Charlie is green.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "green" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All furry, red things are rough.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is green and not round then it is rough.
((("something" "is" "green" "+") ("something" "is" "round" "~")) -> ("something" "is" "rough" "+"))
Green, cold things are rough.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Charlie is not cold.
True
1
proof
[(triple8)]
("Charlie" "is" "cold" "-")
triple8
Charlie is not furry.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "furry" "-")
triple9
Charlie is big.
True
2
proof
[(((triple9) -> rule1))]
("Charlie" "is" "big" "+")
((triple9) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple9) -> rule1))]
("Charlie" "is" "big" "-")
((triple9) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
True
3
proof
[(((((triple9) -> rule1)) -> rule4) OR ((((triple9) -> rule1)) -> rule5))]
("Charlie" "is" "green" "+")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule4) OR ((((triple9) -> rule1)) -> rule5))]
("Charlie" "is" "green" "-")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
@0: Anne is big.[(triple1 OR ((triple3) -> rule1))] Anne is cold.[(triple2)] Anne is furry.[(triple3)] Anne is green.[(triple4 OR ((triple1) -> rule5) OR ((((triple3) -> rule1)) -> rule5))] Anne is red.[(triple5)] Anne is rough.[(triple6 OR ((triple3 triple5) -> rule6) OR ((triple4 triple2) -> rule8) OR ((((triple1) -> rule5) triple2) -> rule8) OR ((((((triple3) -> rule1)) -> rule5) triple2) -> rule8))] Anne is round.[(triple7 OR ((triple2) -> rule3))] Charlie is furry.[(triple9)] Charlie is not cold.[(triple8)] Charlie is red.[(triple10)] Charlie is rough.[(triple11 OR ((triple9 triple10) -> rule6))] Charlie is round.[(triple12)] @1: Charlie is big.[(((triple9) -> rule1))] @2: Charlie is green.[(((((triple9) -> rule1)) -> rule4) OR ((((triple9) -> rule1)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
((triple3 triple5) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple2) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple7
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
((triple9 triple10) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple9) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2