Bob is blue. Bob is nice. Bob is quiet. Charlie is not kind. Charlie is not nice. Charlie is red. Charlie is young. Dave is blue. Dave is not kind. Dave is nice. Dave is smart. Dave is young. If something is young and not smart then it is nice. If something is quiet then it is not kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is young and not smart then it is nice.
((("something" "is" "young" "+") ("something" "is" "smart" "~")) -> ("something" "is" "nice" "+"))
If something is quiet then it is not kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "-"))
Dave is nice.
True
1
proof
[(triple10)]
("Dave" "is" "nice" "+")
triple10
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Bob is not kind.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Charlie is not kind.[(triple4)] Charlie is not nice.[(triple5)] Charlie is red.[(triple6)] Charlie is young.[(triple7)] Dave is blue.[(triple8)] Dave is nice.[(triple10)] Dave is not kind.[(triple9)] Dave is smart.[(triple11)] Dave is young.[(triple12)] @1: Bob is not kind.[(((triple3) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple4
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is not kind.
("Dave" "is" "kind" "-")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Bob is not kind.
("Bob" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1