Anne is blue. Anne is cold. Anne is furry. Anne is quiet. Anne is red. Anne is rough. Anne is smart. All quiet things are cold. All red things are smart. Quiet things are rough. All smart things are red. Rough things are quiet. Furry things are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Anne is smart.
True
1
proof
[(triple7 OR ((triple5) -> rule2))]
("Anne" "is" "smart" "+")
triple7
((triple5) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
1
inv-proof
[(triple7 OR ((triple5) -> rule2))]
("Anne" "is" "smart" "-")
triple7
((triple5) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2 OR ((triple4) -> rule1) OR ((((triple6) -> rule5)) -> rule1) OR ((((((triple3) -> rule6)) -> rule5)) -> rule1))] Anne is furry.[(triple3)] Anne is quiet.[(triple4 OR ((triple6) -> rule5) OR ((((triple3) -> rule6)) -> rule5))] Anne is red.[(triple5 OR ((triple7) -> rule4))] Anne is rough.[(triple6 OR ((triple3) -> rule6) OR ((triple4) -> rule3))] Anne is smart.[(triple7 OR ((triple5) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple6) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple7) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
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
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple5) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1