Anne is furry. Bob is quiet. Charlie is nice. Gary is furry. Nice things are furry. All quiet things are green. Kind things are cold. All green things are kind. If Bob is quiet then Bob is round. All quiet, green things are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Bob is quiet then Bob is round.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "round" "+"))
All quiet, green things are furry.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Charlie is nice.
True
1
proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Bob is green.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Bob is kind.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule6))]
("Bob" "is" "furry" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not cold.
Unknown
inv-rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is furry.[(triple1)] Bob is quiet.[(triple2)] Charlie is nice.[(triple3)] Gary is furry.[(triple4)] @1: Bob is green.[(((triple2) -> rule2))] Bob is round.[(((triple2) -> rule5))] Charlie is furry.[(((triple3) -> rule1))] @2: Bob is furry.[(((triple2 ((triple2) -> rule2)) -> rule6))] Bob is kind.[(((((triple2) -> rule2)) -> rule4))] @3: Bob is cold.[(((((((triple2) -> rule2)) -> rule4)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3