Anne is kind. Anne is quiet. Charlie is furry. Charlie is kind. Dave is kind. Dave is round. Gary is not cold. Gary is furry. Gary is not round. Gary is smart. All kind people are round. If Gary is kind then Gary is cold. If someone is round and not kind then they are smart. If someone is kind and not cold then they are nice. Quiet people are furry. If someone is nice and not round then they are quiet. All smart, cold people are quiet. If Gary is furry then Gary is nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is smart.
("Gary" "is" "smart" "+")
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Gary is kind then Gary is cold.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "cold" "+"))
If someone is round and not kind then they are smart.
((("someone" "is" "round" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "smart" "+"))
If someone is kind and not cold then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is nice and not round then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "quiet" "+"))
All smart, cold people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is furry then Gary is nice.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "nice" "+"))
Dave is kind.
True
1
proof
[(triple5)]
("Dave" "is" "kind" "+")
triple5
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Anne is furry.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "round" "-")
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple8) -> rule8) triple9) -> rule6))]
("Gary" "is" "quiet" "+")
((((triple8) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not quiet.
False
4
inv-proof
[(((((triple8) -> rule8) triple9) -> rule6))]
("Gary" "is" "quiet" "-")
((((triple8) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Charlie is furry.[(triple3)] Charlie is kind.[(triple4)] Dave is kind.[(triple5)] Dave is round.[(triple6 OR ((triple5) -> rule1))] Gary is furry.[(triple8)] Gary is not cold.[(triple7)] Gary is not round.[(triple9)] Gary is smart.[(triple10)] @1: Anne is furry.[(((triple2) -> rule5))] Anne is round.[(((triple1) -> rule1))] Charlie is round.[(((triple4) -> rule1))] Gary is nice.[(((triple8) -> rule8))] @2: Gary is quiet.[(((((triple8) -> rule8) triple9) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
((triple5) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is not cold.
("Gary" "is" "cold" "-")
triple7
Gary is not round.
("Gary" "is" "round" "-")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple8) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple8) -> (rule8 % int2)) triple9) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2