Bob is blue. Bob is nice. Bob is rough. Smart things are rough. If Bob is blue then Bob is quiet. If something is blue and not smart then it is green. If something is smart and not furry then it is green. All furry, nice things are green. If something is rough then it is not green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Bob is blue then Bob is quiet.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "quiet" "+"))
If something is blue and not smart then it is green.
((("something" "is" "blue" "+") ("something" "is" "smart" "~")) -> ("something" "is" "green" "+"))
If something is smart and not furry then it is green.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "green" "+"))
All furry, nice things are green.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is not green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "-"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple3)]
("Bob" "is" "rough" "-")
triple3
Bob is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is rough.[(triple3)] @1: Bob is not green.[(((triple3) -> rule6))] Bob is quiet.[(((triple1) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is not green.
("Bob" "is" "green" "-")
((triple3) -> (rule6 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1