Anne is furry. Anne is green. Anne is quiet. Anne is not round. Bob is quiet. Bob is red. Bob is round. Charlie is furry. Charlie is quiet. Charlie is red. If Anne is nice then Anne is not furry. If Bob is kind then Bob is nice. Nice, quiet things are not kind. If something is red and not nice then it is not round. If something is kind and round then it is red. All quiet things are red. If something is furry then it is red. If something is round and not kind then it is not furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not round.
("Anne" "is" "round" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
If Anne is nice then Anne is not furry.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "-"))
If Bob is kind then Bob is nice.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "nice" "+"))
Nice, quiet things are not kind.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "-"))
If something is red and not nice then it is not round.
((("something" "is" "red" "+") ("something" "is" "nice" "~")) -> ("something" "is" "round" "-"))
If something is kind and round then it is red.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is round and not kind then it is not furry.
((("something" "is" "round" "+") ("something" "is" "kind" "~")) -> ("something" "is" "furry" "-"))
Anne is not round.
True
1
proof
[(triple4)]
("Anne" "is" "round" "-")
triple4
Bob is not round.
False
1
inv-proof
[(triple7)]
("Bob" "is" "round" "-")
triple7
Anne is red.
True
2
proof
[(((triple1) -> rule7) OR ((triple3) -> rule6))]
("Anne" "is" "red" "+")
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple3) -> rule6))]
("Anne" "is" "red" "-")
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is not round.[(triple4)] Anne is quiet.[(triple3)] Bob is quiet.[(triple5)] Bob is red.[(triple6 OR ((triple5) -> rule6))] Bob is round.[(triple7)] Charlie is furry.[(triple8)] Charlie is quiet.[(triple9)] Charlie is red.[(triple10 OR ((triple8) -> rule7) OR ((triple9) -> rule6))] @1: Anne is red.[(((triple1) -> rule7) OR ((triple3) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not round.
("Anne" "is" "round" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
((triple5) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple8) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple9) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1