Bob is blue. Bob is green. Bob is nice. Bob is red. Bob is white. Dave is green. Dave is nice. Dave is red. Dave is white. Dave is young. All furry, nice things are green. White things are blue. White, nice things are young. If something is young and blue then it is nice. Nice, red things are young. If something is young then it is red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All furry, nice things are green.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
White, nice things are young.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is young and blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Nice, red things are young.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Bob is nice.
True
1
proof
[(triple3)]
("Bob" "is" "nice" "+")
triple3
Dave is not green.
False
1
inv-proof
[(triple6)]
("Dave" "is" "green" "-")
triple6
Bob is young.
True
3
proof
[(((triple3 triple4) -> rule5) OR ((triple5 triple3) -> rule3))]
("Bob" "is" "young" "+")
((triple3 triple4) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple9) -> rule2))]
("Dave" "is" "blue" "-")
((triple9) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is blue.[(triple1 OR ((triple5) -> rule2))] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is red.[(triple4 OR ((((triple5 triple3) -> rule3)) -> rule6))] Bob is white.[(triple5)] Dave is green.[(triple6)] Dave is nice.[(triple7 OR ((triple10 ((triple9) -> rule2)) -> rule4))] Dave is red.[(triple8 OR ((triple10) -> rule6) OR ((((triple9 triple7) -> rule3)) -> rule6))] Dave is white.[(triple9)] Dave is young.[(triple10 OR ((triple7 triple8) -> rule5) OR ((triple9 triple7) -> rule3))] @1: Bob is young.[(((triple3 triple4) -> rule5) OR ((triple5 triple3) -> rule3))] Dave is blue.[(((triple9) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((((triple5 triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
((triple10 ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple8
((triple10) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple9 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
((triple7 triple8) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple9 triple7) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple3 triple4) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple9) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1