Anne is blue. Bob is big. Bob is green. Bob is red. Gary is big. Gary is kind. Gary is red. If Bob is kind then Bob is blue. Green, rough people are big. All green people are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
If Bob is kind then Bob is blue.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "blue" "+"))
Green, rough people are big.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Bob is big.
True
1
proof
[(triple2)]
("Bob" "is" "big" "+")
triple2
Gary is not kind.
False
1
inv-proof
[(triple6)]
("Gary" "is" "kind" "-")
triple6
Bob is kind.
True
2
proof
[(((triple3) -> rule3))]
("Bob" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Bob" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Bob is big.[(triple2)] Bob is green.[(triple3)] Bob is red.[(triple4)] Gary is big.[(triple5)] Gary is kind.[(triple6)] Gary is red.[(triple7)] @1: Bob is kind.[(((triple3) -> rule3))] @2: Bob is blue.[(((((triple3) -> rule3)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2