Anne is furry. Anne is not nice. Anne is not round. Anne is smart. Bob is blue. Bob is green. Bob is quiet. Bob is smart. Charlie is blue. Charlie is quiet. If someone is smart and quiet then they are nice. Round people are green. If someone is nice then they are not furry. If Charlie is furry and Charlie is smart then Charlie is not blue. Round people are smart. If someone is quiet and not smart then they are blue.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is not round.
("Anne" "is" "round" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
If someone is smart and quiet then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are not furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
If Charlie is furry and Charlie is smart then Charlie is not blue.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "blue" "-"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and not smart then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "blue" "+"))
Bob is smart.
True
1
proof
[(triple8)]
("Bob" "is" "smart" "+")
triple8
Bob is not quiet.
False
1
inv-proof
[(triple7)]
("Bob" "is" "quiet" "-")
triple7
Bob is nice.
True
3
proof
[(((triple8 triple7) -> rule1))]
("Bob" "is" "nice" "+")
((triple8 triple7) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
3
inv-proof
[(((triple8 triple7) -> rule1))]
("Bob" "is" "nice" "-")
((triple8 triple7) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not furry.
True
4
proof
[(((((triple8 triple7) -> rule1)) -> rule3))]
("Bob" "is" "furry" "-")
((((triple8 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
False
4
inv-proof
[(((((triple8 triple7) -> rule1)) -> rule3))]
("Bob" "is" "furry" "+")
((((triple8 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is furry.[(triple1)] Anne is not nice.[(triple2)] Anne is not round.[(triple3)] Anne is smart.[(triple4)] Bob is blue.[(triple5)] Bob is green.[(triple6)] Bob is quiet.[(triple7)] Bob is smart.[(triple8)] Charlie is blue.[(triple9)] Charlie is quiet.[(triple10)] @1: Bob is nice.[(((triple8 triple7) -> rule1))] @2: Bob is not furry.[(((((triple8 triple7) -> rule1)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is not nice.
("Anne" "is" "nice" "-")
triple2
Anne is not round.
("Anne" "is" "round" "-")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple8
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple8 triple7) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
((((triple8 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2