Bob is round. Charlie is furry. Charlie is nice. Charlie is red. Dave is quiet. Dave is round. Gary is nice. If something is quiet then it is blue. Furry, blue things are rough. If something is red then it is blue. All rough, red things are round. If something is nice and blue then it is red. If Gary is round then Gary is blue. All red, rough things are round. If Bob is nice then Bob is blue.
Bob is round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Furry, blue things are rough.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All rough, red things are round.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is nice and blue then it is red.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If Gary is round then Gary is blue.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "blue" "+"))
All red, rough things are round.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If Bob is nice then Bob is blue.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "blue" "+"))
Dave is round.
True
1
proof
[(triple6)]
("Dave" "is" "round" "+")
triple6
Charlie is not red.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
Charlie is blue.
True
2
proof
[(((triple4) -> rule3))]
("Charlie" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple4) -> rule3))]
("Charlie" "is" "blue" "-")
((triple4) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
True
4
proof
[(((triple2 ((triple4) -> rule3)) -> rule2))]
("Charlie" "is" "rough" "+")
((triple2 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple2 ((triple4) -> rule3)) -> rule2))]
("Charlie" "is" "rough" "-")
((triple2 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
True
6
proof
[(((triple4 ((triple2 ((triple4) -> rule3)) -> rule2)) -> rule7) OR ((((triple2 ((triple4) -> rule3)) -> rule2) triple4) -> rule4))]
("Charlie" "is" "round" "+")
((triple4 ((triple2 ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple2 ((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not round.
False
6
inv-proof
[(((triple4 ((triple2 ((triple4) -> rule3)) -> rule2)) -> rule7) OR ((((triple2 ((triple4) -> rule3)) -> rule2) triple4) -> rule4))]
("Charlie" "is" "round" "-")
((triple4 ((triple2 ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple2 ((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is round.
Unknown
rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is round.[(triple1)] Charlie is furry.[(triple2)] Charlie is nice.[(triple3)] Charlie is red.[(triple4)] Dave is quiet.[(triple5)] Dave is round.[(triple6)] Gary is nice.[(triple7)] @1: Charlie is blue.[(((triple4) -> rule3))] Dave is blue.[(((triple5) -> rule1))] @2: Charlie is rough.[(((triple2 ((triple4) -> rule3)) -> rule2))] @3: Charlie is round.[(((triple4 ((triple2 ((triple4) -> rule3)) -> rule2)) -> rule7) OR ((((triple2 ((triple4) -> rule3)) -> rule2) triple4) -> rule4))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple4 ((triple2 ((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple2 ((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3