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