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