Anne is quiet. Bob is not green. Bob is kind. Bob is nice. Bob is smart. Dave is not blue. Dave is nice. If something is smart then it is not quiet. Big things are nice. If something is blue and not big then it is kind. If something is big and nice then it is blue. All big, smart things are blue. If something is quiet and green then it is not blue. If something is nice and not smart then it is blue. If something is nice and not big then it is green.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is nice.
("Dave" "is" "nice" "+")
If something is smart then it is not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is blue and not big then it is kind.
((("something" "is" "blue" "+") ("something" "is" "big" "~")) -> ("something" "is" "kind" "+"))
If something is big and nice then it is blue.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All big, smart things are blue.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is quiet and green then it is not blue.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "-"))
If something is nice and not smart then it is blue.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "blue" "+"))
If something is nice and not big then it is green.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
Bob is not green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Bob is not quiet.
True
2
proof
[(((triple5) -> rule1))]
("Bob" "is" "quiet" "-")
((triple5) -> (rule1 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is quiet.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Bob is kind.[(triple3)] Bob is nice.[(triple4)] Bob is not green.[(triple2)] Bob is smart.[(triple5)] Dave is nice.[(triple7)] Dave is not blue.[(triple6)] @1: Bob is not quiet.[(((triple5) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is not blue.
("Dave" "is" "blue" "-")
triple6
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple5) -> (rule1 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1