Bob is furry. Bob is red. Bob is rough. If Bob is nice and Bob is red then Bob is big. All white, quiet people are big. If someone is nice then they are rough. If Bob is white then Bob is big. Rough, white people are furry. If someone is furry and rough then they are white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
If Bob is nice and Bob is red then Bob is big.
((("Bob" "is" "nice" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "big" "+"))
All white, quiet people are big.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Bob is white then Bob is big.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "big" "+"))
Rough, white people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and rough then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Bob is not rough.
False
1
inv-proof
[(triple3)]
("Bob" "is" "rough" "-")
triple3
Bob is white.
True
3
proof
[(((triple1 triple3) -> rule6))]
("Bob" "is" "white" "+")
((triple1 triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
3
inv-proof
[(((triple1 triple3) -> rule6))]
("Bob" "is" "white" "-")
((triple1 triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3)] @1: Bob is white.[(((triple1 triple3) -> rule6))] @2: Bob is big.[(((((triple1 triple3) -> rule6)) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1 triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2