The cow eats the dog. The cow likes the mouse. The dog eats the squirrel. The dog likes the cow. The dog likes the mouse. The dog visits the cow. The mouse eats the dog. The squirrel is green. The squirrel is round. The squirrel likes the mouse. The squirrel visits the dog. The squirrel visits the mouse. If someone is round then they like the squirrel. If someone is round and they like the squirrel then the squirrel eats the dog. If someone eats the cow then the cow likes the squirrel. If the cow eats the dog and the cow is big then the cow likes the squirrel. If someone eats the mouse then they are round. If the squirrel likes the dog then the dog likes the mouse. If someone is blue and green then they are nice. If someone eats the dog and they are round then the dog eats the mouse.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone is round then they like the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone is round and they like the squirrel then the squirrel eats the dog.
((("someone" "is" "round" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "eats" "dog" "+"))
If someone eats the cow then the cow likes the squirrel.
((("someone" "eats" "cow" "+")) -> ("cow" "likes" "squirrel" "+"))
If the cow eats the dog and the cow is big then the cow likes the squirrel.
((("cow" "eats" "dog" "+") ("cow" "is" "big" "+")) -> ("cow" "likes" "squirrel" "+"))
If someone eats the mouse then they are round.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "round" "+"))
If the squirrel likes the dog then the dog likes the mouse.
((("squirrel" "likes" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
If someone is blue and green then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the dog and they are round then the dog eats the mouse.
((("someone" "eats" "dog" "+") ("someone" "is" "round" "+")) -> ("dog" "eats" "mouse" "+"))
The squirrel is round.
True
1
proof
[(triple9)]
("squirrel" "is" "round" "+")
triple9
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple12)]
("squirrel" "visits" "mouse" "-")
triple12
The squirrel likes the squirrel.
True
2
proof
[(((triple9) -> rule1))]
("squirrel" "likes" "squirrel" "+")
((triple9) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple9) -> rule1))]
("squirrel" "likes" "squirrel" "-")
((triple9) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the dog.
True
4
proof
[(((triple9 ((triple9) -> rule1)) -> rule2))]
("squirrel" "eats" "dog" "+")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel does not eat the dog.
False
4
inv-proof
[(((triple9 ((triple9) -> rule1)) -> rule2))]
("squirrel" "eats" "dog" "-")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The dog eats the mouse.
True
6
proof
[(((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8))]
("dog" "eats" "mouse" "+")
((((triple9 ((triple9) -> (rule1 % int3))) -> (rule2 % int2)) triple9) -> (rule8 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The dog does not eat the mouse.
False
6
inv-proof
[(((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8))]
("dog" "eats" "mouse" "-")
((((triple9 ((triple9) -> (rule1 % int3))) -> (rule2 % int2)) triple9) -> (rule8 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The dog is round.
True
7
proof
[(((((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8)) -> rule5))]
("dog" "is" "round" "+")
((((((triple9 ((triple9) -> (rule1 % int4))) -> (rule2 % int3)) triple9) -> (rule8 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The dog is not round.
False
7
inv-proof
[(((((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8)) -> rule5))]
("dog" "is" "round" "-")
((((((triple9 ((triple9) -> (rule1 % int4))) -> (rule2 % int3)) triple9) -> (rule8 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The dog likes the squirrel.
True
8
proof
[(((((((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8)) -> rule5)) -> rule1))]
("dog" "likes" "squirrel" "+")
((((((((triple9 ((triple9) -> (rule1 % int5))) -> (rule2 % int4)) triple9) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5
The dog does not like the squirrel.
False
8
inv-proof
[(((((((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8)) -> rule5)) -> rule1))]
("dog" "likes" "squirrel" "-")
((((((((triple9 ((triple9) -> (rule1 % int5))) -> (rule2 % int4)) triple9) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "nice" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "nice" "+")
The cow does not like the squirrel.
Unknown
inv-rconc
[@2: The cow likes the squirrel.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("cow" "likes" "squirrel" "-")
The mouse likes the squirrel.
Unknown
rconc
[@2: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "round" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "nice" "+")
The mouse does not eat the squirrel.
Unknown
inv-random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The dog does not visit the squirrel.
Unknown
inv-random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The cow eats the dog.[(triple1)] The cow likes the mouse.[(triple2)] The dog eats the squirrel.[(triple3)] The dog likes the cow.[(triple4)] The dog likes the mouse.[(triple5)] The dog visits the cow.[(triple6)] The mouse eats the dog.[(triple7)] The squirrel is green.[(triple8)] The squirrel is round.[(triple9)] The squirrel likes the mouse.[(triple10)] The squirrel visits the dog.[(triple11)] The squirrel visits the mouse.[(triple12)] @1: The squirrel likes the squirrel.[(((triple9) -> rule1))] @2: The squirrel eats the dog.[(((triple9 ((triple9) -> rule1)) -> rule2))] @3: The dog eats the mouse.[(((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8))] @4: The dog is round.[(((((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8)) -> rule5))] @5: The dog likes the squirrel.[(((((((((triple9 ((triple9) -> rule1)) -> rule2) triple9) -> rule8)) -> rule5)) -> rule1))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple3
The dog likes the cow.
("dog" "likes" "cow" "+")
triple4
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple10
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple11
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple9) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((((triple9 ((triple9) -> (rule1 % int3))) -> (rule2 % int2)) triple9) -> (rule8 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int3
The dog is round.
("dog" "is" "round" "+")
((((((triple9 ((triple9) -> (rule1 % int4))) -> (rule2 % int3)) triple9) -> (rule8 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int4
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((((((((triple9 ((triple9) -> (rule1 % int5))) -> (rule2 % int4)) triple9) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int5