Anne is green. Charlie is big. Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is young. Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is young. Gary is furry. Gary is young. Big things are green. All furry things are nice. All young, nice things are big.
Anne is green.
("Anne" "is" "green" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is young.
("Gary" "is" "young" "+")
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All young, nice things are big.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Charlie is nice.
True
1
proof
[(triple6 OR ((triple3) -> rule2))]
("Charlie" "is" "nice" "+")
triple6
((triple3) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "kind" "-")
triple5
Gary is nice.
True
2
proof
[(((triple15) -> rule2))]
("Gary" "is" "nice" "+")
((triple15) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple15) -> rule2))]
("Gary" "is" "nice" "-")
((triple15) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
True
4
proof
[(((triple16 ((triple15) -> rule2)) -> rule3))]
("Gary" "is" "big" "+")
((triple16 ((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not big.
False
4
inv-proof
[(((triple16 ((triple15) -> rule2)) -> rule3))]
("Gary" "is" "big" "-")
((triple16 ((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is green.
True
5
proof
[(((((triple16 ((triple15) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "green" "+")
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not green.
False
5
inv-proof
[(((((triple16 ((triple15) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "green" "-")
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is green.[(triple1)] Charlie is big.[(triple2 OR ((triple7 triple6) -> rule3) OR ((triple7 ((triple3) -> rule2)) -> rule3))] Charlie is furry.[(triple3)] Charlie is green.[(triple4 OR ((triple2) -> rule1) OR ((((triple7 triple6) -> rule3)) -> rule1) OR ((((triple7 ((triple3) -> rule2)) -> rule3)) -> rule1))] Charlie is kind.[(triple5)] Charlie is nice.[(triple6 OR ((triple3) -> rule2))] Charlie is young.[(triple7)] Dave is big.[(triple8 OR ((triple14 triple12) -> rule3) OR ((triple14 ((triple9) -> rule2)) -> rule3))] Dave is furry.[(triple9)] Dave is green.[(triple10 OR ((triple8) -> rule1) OR ((((triple14 triple12) -> rule3)) -> rule1) OR ((((triple14 ((triple9) -> rule2)) -> rule3)) -> rule1))] Dave is kind.[(triple11)] Dave is nice.[(triple12 OR ((triple9) -> rule2))] Dave is quiet.[(triple13)] Dave is young.[(triple14)] Gary is furry.[(triple15)] Gary is young.[(triple16)] @1: Gary is nice.[(((triple15) -> rule2))] @2: Gary is big.[(((triple16 ((triple15) -> rule2)) -> rule3))] @3: Gary is green.[(((((triple16 ((triple15) -> rule2)) -> rule3)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
((triple7 triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple7 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple3) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
((triple14 triple12) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple14 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
((triple8) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple14 triple12) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple14 ((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
((triple9) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Dave is young.
("Dave" "is" "young" "+")
triple14
Gary is furry.
("Gary" "is" "furry" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Gary is nice.
("Gary" "is" "nice" "+")
((triple15) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple16 ((triple15) -> (rule2 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple16 ((triple15) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3