Anne is big. Anne is cold. Anne is quiet. Anne is red. Bob is red. Bob is smart. Charlie is cold. If Bob is young then Bob is quiet. All red things are smart. All smart, red things are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
If Bob is young then Bob is quiet.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "quiet" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All smart, red things are quiet.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Charlie is cold.
True
1
proof
[(triple7)]
("Charlie" "is" "cold" "+")
triple7
Anne is not quiet.
False
1
inv-proof
[(triple3 OR ((((triple4) -> rule2) triple4) -> rule3))]
("Anne" "is" "quiet" "-")
triple3
((((triple4) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is quiet.[(triple3 OR ((((triple4) -> rule2) triple4) -> rule3))] Anne is red.[(triple4)] Bob is red.[(triple5)] Bob is smart.[(triple6 OR ((triple5) -> rule2))] Charlie is cold.[(triple7)] @1: Anne is smart.[(((triple4) -> rule2))] Bob is quiet.[(((triple6 triple5) -> rule3) OR ((((triple5) -> rule2) triple5) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((((triple4) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple5) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple6 triple5) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2