Bob is quiet. Bob is red. Charlie is not green. Charlie is kind. Charlie is not quiet. Charlie is white. Gary is kind. Gary is quiet. Gary is red. Gary is white. Harry is blue. Harry is red. If someone is green and not kind then they are quiet. All blue people are not rough. If someone is kind and not white then they are green.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is green and not kind then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "quiet" "+"))
All blue people are not rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
If someone is kind and not white then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "+"))
Harry is red.
True
1
proof
[(triple12)]
("Harry" "is" "red" "+")
triple12
Charlie is not kind.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "kind" "-")
triple4
Harry is not rough.
True
2
proof
[(((triple11) -> rule2))]
("Harry" "is" "rough" "-")
((triple11) -> (rule2 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is rough.
False
2
inv-proof
[(((triple11) -> rule2))]
("Harry" "is" "rough" "+")
((triple11) -> (rule2 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Bob is quiet.[(triple1)] Bob is red.[(triple2)] Charlie is kind.[(triple4)] Charlie is not green.[(triple3)] Charlie is not quiet.[(triple5)] Charlie is white.[(triple6)] Gary is kind.[(triple7)] Gary is quiet.[(triple8)] Gary is red.[(triple9)] Gary is white.[(triple10)] Harry is blue.[(triple11)] Harry is red.[(triple12)] @1: Harry is not rough.[(((triple11) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not green.
("Charlie" "is" "green" "-")
triple3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is not rough.
("Harry" "is" "rough" "-")
((triple11) -> (rule2 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1