Anne is nice. Bob is green. Bob is not nice. Dave is big. Dave is blue. Dave is nice. Gary is red. All red things are big. If something is green then it is red.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Bob is not nice.
True
1
proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Dave is not nice.
False
1
inv-proof
[(triple6)]
("Dave" "is" "nice" "-")
triple6
Gary is big.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "big" "+")
((triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "red" "-")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is nice.[(triple1)] Bob is green.[(triple2)] Bob is not nice.[(triple3)] Dave is big.[(triple4)] Dave is blue.[(triple5)] Dave is nice.[(triple6)] Gary is red.[(triple7)] @1: Bob is red.[(((triple2) -> rule2))] Gary is big.[(((triple7) -> rule1))] @2: Bob is big.[(((((triple2) -> rule2)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2