Bob is big. Bob is furry. Bob is nice. Round things are rough. All red things are rough. All round, big things are furry. If something is round then it is red. If Bob is big then Bob is nice. If something is furry then it is red. If something is rough and furry then it is red. Round things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All round, big things are furry.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If Bob is big then Bob is nice.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "nice" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is rough and furry then it is red.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is red.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "red" "+")
((triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "red" "-")
((triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3 OR ((triple1) -> rule5))] @1: Bob is red.[(((triple2) -> rule6))] @2: Bob is rough.[(((((triple2) -> rule6)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2