Anne is kind. Anne is nice. Anne is young. Bob is blue. Bob is nice. Bob is white. Gary is red. Gary is young. Harry is nice. Harry is white. If someone is white then they are red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Gary is red.
True
1
proof
[(triple7)]
("Gary" "is" "red" "+")
triple7
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Bob is red.
True
2
proof
[(((triple6) -> rule1))]
("Bob" "is" "red" "+")
((triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple6) -> rule1))]
("Bob" "is" "red" "-")
((triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Anne is young.[(triple3)] Bob is blue.[(triple4)] Bob is nice.[(triple5)] Bob is white.[(triple6)] Gary is red.[(triple7)] Gary is young.[(triple8)] Harry is nice.[(triple9)] Harry is white.[(triple10)] @1: Bob is red.[(((triple6) -> rule1))] Harry is red.[(((triple10) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Gary is young.
("Gary" "is" "young" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is red.
("Bob" "is" "red" "+")
((triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1