Bob is blue. Bob is rough. Bob is round. Bob is smart. Dave is blue. Dave is green. Dave is nice. Dave is red. Dave is not rough. Dave is round. Round people are red. Red, blue people are green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red, blue people are green.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Dave is green.
True
1
proof
[(triple6 OR ((triple8 triple5) -> rule2) OR ((((triple10) -> rule1) triple5) -> rule2))]
("Dave" "is" "green" "+")
triple6
((triple8 triple5) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple10) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not blue.
False
1
inv-proof
[(triple5)]
("Dave" "is" "blue" "-")
triple5
Bob is red.
True
2
proof
[(((triple3) -> rule1))]
("Bob" "is" "red" "+")
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "red" "-")
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
True
4
proof
[(((((triple3) -> rule1) triple1) -> rule2))]
("Bob" "is" "green" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not green.
False
4
inv-proof
[(((((triple3) -> rule1) triple1) -> rule2))]
("Bob" "is" "green" "-")
((((triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2)] Bob is round.[(triple3)] Bob is smart.[(triple4)] Dave is blue.[(triple5)] Dave is green.[(triple6 OR ((triple8 triple5) -> rule2) OR ((((triple10) -> rule1) triple5) -> rule2))] Dave is nice.[(triple7)] Dave is not rough.[(triple9)] Dave is red.[(triple8 OR ((triple10) -> rule1))] Dave is round.[(triple10)] @1: Bob is red.[(((triple3) -> rule1))] @2: Bob is green.[(((((triple3) -> rule1) triple1) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
((triple8 triple5) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple10) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is not rough.
("Dave" "is" "rough" "-")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple8
((triple10) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2