Anne is not cold. Anne is quiet. Anne is rough. Anne is smart. Bob is kind. Bob is quiet. Bob is rough. Bob is white. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is not rough. Charlie is smart. Gary is cold. Gary is white. All rough people are smart.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Bob is smart.
True
2
proof
[(((triple7) -> rule1))]
("Bob" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple7) -> rule1))]
("Bob" "is" "smart" "-")
((triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is not cold.[(triple1)] Anne is quiet.[(triple2)] Anne is rough.[(triple3)] Anne is smart.[(triple4 OR ((triple3) -> rule1))] Bob is kind.[(triple5)] Bob is quiet.[(triple6)] Bob is rough.[(triple7)] Bob is white.[(triple8)] Charlie is green.[(triple9)] Charlie is kind.[(triple10)] Charlie is not rough.[(triple12)] Charlie is quiet.[(triple11)] Charlie is smart.[(triple13)] Gary is cold.[(triple14)] Gary is white.[(triple15)] @1: Bob is smart.[(((triple7) -> rule1))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple3) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Bob is rough.
("Bob" "is" "rough" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple12
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
Charlie is smart.
("Charlie" "is" "smart" "+")
triple13
Gary is cold.
("Gary" "is" "cold" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Bob is smart.
("Bob" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1