Bob is furry. Charlie is furry. Dave is nice. Erin is not red. All smart, blue things are furry. If Erin is smart and Erin is blue then Erin is nice. If something is furry then it is kind. If Bob is red then Bob is rough. If Erin is rough and Erin is kind then Erin is not blue. Kind things are rough. If something is kind then it is blue. If Dave is nice and Dave is blue then Dave is not red.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is not red.
("Erin" "is" "red" "-")
All smart, blue things are furry.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If Erin is smart and Erin is blue then Erin is nice.
((("Erin" "is" "smart" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "nice" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
If Erin is rough and Erin is kind then Erin is not blue.
((("Erin" "is" "rough" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "blue" "-"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Dave is nice and Dave is blue then Dave is not red.
((("Dave" "is" "nice" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "-"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Bob is kind.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("Charlie" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule7))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not kind.
Unknown
inv-rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is furry.[(triple1)] Charlie is furry.[(triple2)] Dave is nice.[(triple3)] Erin is not red.[(triple4)] @1: Bob is kind.[(((triple1) -> rule3))] Charlie is kind.[(((triple2) -> rule3))] @2: Bob is blue.[(((((triple1) -> rule3)) -> rule7))] Bob is rough.[(((((triple1) -> rule3)) -> rule6))] Charlie is blue.[(((((triple2) -> rule3)) -> rule7))] Charlie is rough.[(((((triple2) -> rule3)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Erin is not red.
("Erin" "is" "red" "-")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2