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