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