Bob is big. Dave is green. Erin is white. Harry is white. Big things are not furry. If something is green and not kind then it is white.
Bob is big.
("Bob" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
Big things are not furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "-"))
If something is green and not kind then it is white.
((("something" "is" "green" "+") ("something" "is" "kind" "~")) -> ("something" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is not furry.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is big.[(triple1)] Dave is green.[(triple2)] Erin is white.[(triple3)] Harry is white.[(triple4)] @1: Bob is not furry.[(((triple1) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Bob is not furry.
("Bob" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1