Anne is big. Anne is nice. Anne is red. Anne is white. Anne is not young. Bob is kind. Bob is nice. Bob is red. Bob is white. Bob is young. Dave is nice. Dave is white. Dave is young. Gary is not big. Gary is white. All green people are young. All young, big people are green. If someone is kind then they are big. If someone is nice and green then they are big. Young people are kind. If someone is young and not green then they are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is not young.
("Anne" "is" "young" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is white.
("Gary" "is" "white" "+")
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All young, big people are green.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and green then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and not green then they are white.
((("someone" "is" "young" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "+"))
Gary is white.
True
1
proof
[(triple15)]
("Gary" "is" "white" "+")
triple15
Bob is not red.
False
1
inv-proof
[(triple8)]
("Bob" "is" "red" "-")
triple8
Dave is kind.
True
2
proof
[(((triple13) -> rule5))]
("Dave" "is" "kind" "+")
((triple13) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple10) -> rule5)) -> rule3))]
("Bob" "is" "big" "-")
((triple6) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is big.
True
3
proof
[(((((triple13) -> rule5)) -> rule3))]
("Dave" "is" "big" "+")
((((triple13) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Bob is not green.
False
4
inv-proof
[(((triple10 ((triple6) -> rule3)) -> rule2) OR ((triple10 ((((triple10) -> rule5)) -> rule3)) -> rule2))]
("Bob" "is" "green" "-")
((triple10 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple10 ((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Dave is green.
True
5
proof
[(((triple13 ((((triple13) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "green" "+")
((triple13 ((((triple13) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not green.
False
5
inv-proof
[(((triple13 ((((triple13) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "green" "-")
((triple13 ((((triple13) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Gary is not kind.
Unknown
inv-rconc
[@3: Gary is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Anne is not young.[(triple5)] Anne is red.[(triple3)] Anne is white.[(triple4)] Bob is kind.[(triple6 OR ((triple10) -> rule5))] Bob is nice.[(triple7)] Bob is red.[(triple8)] Bob is white.[(triple9)] Bob is young.[(triple10)] Dave is nice.[(triple11)] Dave is white.[(triple12)] Dave is young.[(triple13)] Gary is not big.[(triple14)] Gary is white.[(triple15)] @1: Bob is big.[(((triple6) -> rule3) OR ((((triple10) -> rule5)) -> rule3))] Dave is kind.[(((triple13) -> rule5))] @2: Bob is green.[(((triple10 ((triple6) -> rule3)) -> rule2) OR ((triple10 ((((triple10) -> rule5)) -> rule3)) -> rule2))] Dave is big.[(((((triple13) -> rule5)) -> rule3))] @3: Dave is green.[(((triple13 ((((triple13) -> rule5)) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not young.
("Anne" "is" "young" "-")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple6
((triple10) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
triple8
Bob is white.
("Bob" "is" "white" "+")
triple9
Bob is young.
("Bob" "is" "young" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
triple13
Gary is not big.
("Gary" "is" "big" "-")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Bob is big.
("Bob" "is" "big" "+")
((triple6) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple13) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple10 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple10 ((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((triple13) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple13 ((((triple13) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3