Bob is red. Dave is rough. Gary is furry. If someone is furry then they are quiet. If Bob is red and Bob is white then Bob is nice. If Gary is blue then Gary is rough. If Gary is quiet then Gary is rough. All red people are blue. If someone is red then they are blue. If someone is rough and blue then they are not nice. Rough people are white.
Bob is red.
("Bob" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is red and Bob is white then Bob is nice.
((("Bob" "is" "red" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "nice" "+"))
If Gary is blue then Gary is rough.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is quiet then Gary is rough.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "rough" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and blue then they are not nice.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Gary is furry.
True
1
proof
[(triple3)]
("Gary" "is" "furry" "+")
triple3
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is blue.
True
2
proof
[(((triple1) -> rule5) OR ((triple1) -> rule6))]
("Bob" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1) -> rule6))]
("Bob" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Gary" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Gary" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
True
4
proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule8))]
("Gary" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule8))]
("Gary" "is" "white" "-")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "white" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is red.[(triple1)] Dave is rough.[(triple2)] Gary is furry.[(triple3)] @1: Bob is blue.[(((triple1) -> rule5) OR ((triple1) -> rule6))] Dave is white.[(((triple2) -> rule8))] Gary is quiet.[(((triple3) -> rule1))] @2: Gary is rough.[(((((triple3) -> rule1)) -> rule4))] @3: Gary is white.[(((((((triple3) -> rule1)) -> rule4)) -> rule8))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3