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