Charlie is furry. Charlie is quiet. Charlie is red. Charlie is round. Fiona is furry. Fiona is quiet. Fiona is round. Fiona is white. Fiona is young. Gary is furry. Gary is quiet. Gary is red. Round things are furry. Quiet, young things are big. If Charlie is red and Charlie is young then Charlie is quiet. If something is round and furry then it is young. Furry things are quiet. All red, round things are young.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Quiet, young things are big.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Charlie is red and Charlie is young then Charlie is quiet.
((("Charlie" "is" "red" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is round and furry then it is young.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All red, round things are young.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Fiona is round.
True
1
proof
[(triple7)]
("Fiona" "is" "round" "+")
triple7
Fiona is not quiet.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule5) OR ((((triple7) -> rule1)) -> rule5))]
("Fiona" "is" "quiet" "-")
triple6
((triple5) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is furry.[(triple1 OR ((triple4) -> rule1))] Charlie is quiet.[(triple2 OR ((triple1) -> rule5) OR ((((triple4) -> rule1)) -> rule5) OR ((triple3 ((triple3 triple4) -> rule6)) -> rule3) OR ((triple3 ((triple4 triple1) -> rule4)) -> rule3) OR ((triple3 ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule3))] Charlie is red.[(triple3)] Charlie is round.[(triple4)] Fiona is furry.[(triple5 OR ((triple7) -> rule1))] Fiona is quiet.[(triple6 OR ((triple5) -> rule5) OR ((((triple7) -> rule1)) -> rule5))] Fiona is round.[(triple7)] Fiona is white.[(triple8)] Fiona is young.[(triple9 OR ((triple7 triple5) -> rule4) OR ((triple7 ((triple7) -> rule1)) -> rule4))] Gary is furry.[(triple10)] Gary is quiet.[(triple11 OR ((triple10) -> rule5))] Gary is red.[(triple12)] @1: Charlie is young.[(((triple3 triple4) -> rule6) OR ((triple4 triple1) -> rule4) OR ((triple4 ((triple4) -> rule1)) -> rule4))] Fiona is big.[(((triple6 triple9) -> rule2) OR ((triple6 ((triple7 triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule5) triple9) -> rule2) OR ((((triple5) -> rule5) ((triple7 triple5) -> rule4)) -> rule2) OR ((triple6 ((triple7 ((triple7) -> rule1)) -> rule4)) -> rule2) OR ((((((triple7) -> rule1)) -> rule5) triple9) -> rule2) OR ((((triple5) -> rule5) ((triple7 ((triple7) -> rule1)) -> rule4)) -> rule2) OR ((((((triple7) -> rule1)) -> rule5) ((triple7 triple5) -> rule4)) -> rule2) OR ((((((triple7) -> rule1)) -> rule5) ((triple7 ((triple7) -> rule1)) -> rule4)) -> rule2))] @2: Charlie is big.[(((triple2 ((triple3 triple4) -> rule6)) -> rule2) OR ((triple2 ((triple4 triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule5) ((triple3 triple4) -> rule6)) -> rule2) OR ((((triple1) -> rule5) ((triple4 triple1) -> rule4)) -> rule2) OR ((triple2 ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule2) OR ((((triple1) -> rule5) ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule2) OR ((((((triple4) -> rule1)) -> rule5) ((triple3 triple4) -> rule6)) -> rule2) OR ((((((triple4) -> rule1)) -> rule5) ((triple4 triple1) -> rule4)) -> rule2) OR ((((triple3 ((triple3 triple4) -> rule6)) -> rule3) ((triple3 triple4) -> rule6)) -> rule2) OR ((((triple3 ((triple3 triple4) -> rule6)) -> rule3) ((triple4 triple1) -> rule4)) -> rule2) OR ((((triple3 ((triple4 triple1) -> rule4)) -> rule3) ((triple3 triple4) -> rule6)) -> rule2) OR ((((triple3 ((triple4 triple1) -> rule4)) -> rule3) ((triple4 triple1) -> rule4)) -> rule2) OR ((((((triple4) -> rule1)) -> rule5) ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule2) OR ((((triple3 ((triple3 triple4) -> rule6)) -> rule3) ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule2) OR ((((triple3 ((triple4 triple1) -> rule4)) -> rule3) ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule2) OR ((((triple3 ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule3) ((triple3 triple4) -> rule6)) -> rule2) OR ((((triple3 ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule3) ((triple4 triple1) -> rule4)) -> rule2) OR ((((triple3 ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule3) ((triple4 ((triple4) -> rule1)) -> rule4)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((triple3 ((triple3 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple3 ((triple4 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple3 ((triple4 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
((triple7) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
((triple5) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
((triple7 triple5) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
((triple10) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple12
Charlie is young.
("Charlie" "is" "young" "+")
((triple3 triple4) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple6 triple9) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple6 ((triple7 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple5) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple7 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((triple6 ((triple7 ((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((triple5) -> (rule5 % int4)) ((triple7 ((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
((((((triple7) -> (rule1 % int4))) -> (rule5 % int3)) ((triple7 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
((((((triple7) -> (rule1 % int4))) -> (rule5 % int3)) ((triple7 ((triple7) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 ((triple3 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple2 ((triple4 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple3 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple1) -> (rule5 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple2 ((triple4 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((triple1) -> (rule5 % int4)) ((triple4 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple4) -> (rule1 % int4))) -> (rule5 % int3)) ((triple3 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((((triple4) -> (rule1 % int4))) -> (rule5 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple3 ((triple3 triple4) -> (rule6 % int3))) -> (rule3 % int2)) ((triple3 triple4) -> (rule6 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple3 ((triple3 triple4) -> (rule6 % int3))) -> (rule3 % int2)) ((triple4 triple1) -> (rule4 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple3 ((triple4 triple1) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3 triple4) -> (rule6 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple3 ((triple4 triple1) -> (rule4 % int3))) -> (rule3 % int2)) ((triple4 triple1) -> (rule4 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple4) -> (rule1 % int4))) -> (rule5 % int3)) ((triple4 ((triple4) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple3 ((triple3 triple4) -> (rule6 % int4))) -> (rule3 % int3)) ((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int4))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((triple3 ((triple4 triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int4))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((triple3 ((triple4 ((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3 triple4) -> (rule6 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple3 ((triple4 ((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2)) ((triple4 triple1) -> (rule4 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((triple3 ((triple4 ((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2)) ((triple4 ((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4