Anne is furry. Charlie is big. Charlie is quiet. If someone is quiet then they are cold. All quiet people are white. Furry, quiet people are smart. If someone is cold then they are rough. If someone is furry and white then they are rough. If someone is big then they are quiet. Rough, big people are quiet. If Charlie is white and Charlie is smart then Charlie is quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Furry, quiet people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry and white then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Rough, big people are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is white and Charlie is smart then Charlie is quiet.
((("Charlie" "is" "white" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "quiet" "+"))
Charlie is quiet.
True
1
proof
[(triple3 OR ((triple2) -> rule6))]
("Charlie" "is" "quiet" "+")
triple3
((triple2) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Charlie is cold.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2) -> rule6)) -> rule1))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple2) -> rule6)) -> rule1))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Anne" "is" "white" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Charlie is quiet.[(triple3 OR ((triple2) -> rule6))] @1: Charlie is cold.[(((triple3) -> rule1) OR ((((triple2) -> rule6)) -> rule1))] Charlie is white.[(((triple3) -> rule2) OR ((((triple2) -> rule6)) -> rule2))] @2: Charlie is rough.[(((((triple3) -> rule1)) -> rule4) OR ((((((triple2) -> rule6)) -> rule1)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple2) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple3) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3