Bob is cold. Bob is green. Bob is nice. Bob is white. Dave is blue. Dave is green. Dave is white. If something is round and blue then it is not cold. If something is white then it is nice. Nice things are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is round and blue then it is not cold.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Dave is nice.
True
2
proof
[(((triple7) -> rule2))]
("Dave" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple7) -> rule2))]
("Dave" "is" "nice" "-")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Dave" "is" "rough" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Dave" "is" "rough" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple4) -> rule2))] Bob is white.[(triple4)] Dave is blue.[(triple5)] Dave is green.[(triple6)] Dave is white.[(triple7)] @1: Bob is rough.[(((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))] Dave is nice.[(((triple7) -> rule2))] @2: Dave is rough.[(((((triple7) -> rule2)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2