Anne is blue. Anne is kind. Anne is quiet. Bob is kind. Bob is not quiet. Bob is white. Bob is young. Dave is blue. Dave is kind. Dave is not quiet. Dave is white. Dave is young. If something is quiet and big then it is green. If something is blue and not kind then it is green. If something is kind and white then it is big. Quiet things are big. If Anne is young and Anne is big then Anne is quiet. All green things are white. If Bob is white and Bob is not kind then Bob is green. Quiet, green things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is quiet and big then it is green.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is blue and not kind then it is green.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "green" "+"))
If something is kind and white then it is big.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Anne is young and Anne is big then Anne is quiet.
((("Anne" "is" "young" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "quiet" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Bob is white and Bob is not kind then Bob is green.
((("Bob" "is" "white" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "green" "+"))
Quiet, green things are blue.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((triple3 ((triple3 ((triple3) -> rule4)) -> rule1)) -> rule8))]
("Anne" "is" "blue" "+")
triple1
((triple3 ((triple3 ((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is not blue.
False
1
inv-proof
[(triple8)]
("Dave" "is" "blue" "-")
triple8
Bob is big.
True
3
proof
[(((triple4 triple6) -> rule3))]
("Bob" "is" "big" "+")
((triple4 triple6) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is not big.
False
3
inv-proof
[(((triple9 triple11) -> rule3))]
("Dave" "is" "big" "-")
((triple9 triple11) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is green.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule1))]
("Anne" "is" "green" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not green.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule1))]
("Anne" "is" "green" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
True
5
proof
[(((((triple3 ((triple3) -> rule4)) -> rule1)) -> rule6))]
("Anne" "is" "white" "+")
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not white.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule4)) -> rule1)) -> rule6))]
("Anne" "is" "white" "-")
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is blue.[(triple1 OR ((triple3 ((triple3 ((triple3) -> rule4)) -> rule1)) -> rule8))] Anne is kind.[(triple2)] Anne is quiet.[(triple3)] Bob is kind.[(triple4)] Bob is not quiet.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7)] Dave is blue.[(triple8)] Dave is kind.[(triple9)] Dave is not quiet.[(triple10)] Dave is white.[(triple11)] Dave is young.[(triple12)] @1: Anne is big.[(((triple3) -> rule4))] Bob is big.[(((triple4 triple6) -> rule3))] Dave is big.[(((triple9 triple11) -> rule3))] @2: Anne is green.[(((triple3 ((triple3) -> rule4)) -> rule1))] @3: Anne is white.[(((((triple3 ((triple3) -> rule4)) -> rule1)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple3 ((triple3 ((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple4 triple6) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple9 triple11) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3