Bob is green. If something is big then it is furry. All green things are not white. If something is big then it is white. All green things are not big. If Bob is big then Bob is not furry. If something is furry and not white then it is not quiet. If something is big and furry then it is rough. If something is cold and not furry then it is rough.
Bob is green.
("Bob" "is" "green" "+")
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All green things are not white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "-"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All green things are not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If Bob is big then Bob is not furry.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "furry" "-"))
If something is furry and not white then it is not quiet.
((("something" "is" "furry" "+") ("something" "is" "white" "~")) -> ("something" "is" "quiet" "-"))
If something is big and furry then it is rough.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is cold and not furry then it is rough.
((("something" "is" "cold" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Bob is not white.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "white" "-")
((triple1) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is big.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "big" "+")
((triple1) -> (rule4 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1)] @1: Bob is not big.[(((triple1) -> rule4))] Bob is not white.[(((triple1) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not big.
("Bob" "is" "big" "-")
((triple1) -> (rule4 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is not white.
("Bob" "is" "white" "-")
((triple1) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1