The cow needs the squirrel. The cow needs the tiger. The cow sees the dog. The dog chases the squirrel. The dog is big. The dog needs the squirrel. The squirrel is blue. The squirrel is green. The squirrel needs the tiger. The squirrel sees the dog. The squirrel sees the tiger. The tiger chases the cow. The tiger needs the cow. The tiger needs the squirrel. The tiger sees the dog. If the cow is cold then the cow chases the squirrel. All blue, cold people are round. If someone chases the squirrel and they are big then they are round. If the squirrel chases the cow and the squirrel needs the cow then the cow is green. If someone sees the tiger then they chase the cow. If someone is big and they chase the tiger then the tiger needs the dog. If someone chases the squirrel then they see the tiger. If someone needs the tiger and they chase the cow then the tiger chases the squirrel.
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is big.
("dog" "is" "big" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If the cow is cold then the cow chases the squirrel.
((("cow" "is" "cold" "+")) -> ("cow" "chases" "squirrel" "+"))
All blue, cold people are round.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone chases the squirrel and they are big then they are round.
((("someone" "chases" "squirrel" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If the squirrel chases the cow and the squirrel needs the cow then the cow is green.
((("squirrel" "chases" "cow" "+") ("squirrel" "needs" "cow" "+")) -> ("cow" "is" "green" "+"))
If someone sees the tiger then they chase the cow.
((("someone" "sees" "tiger" "+")) -> ("someone" "chases" "cow" "+"))
If someone is big and they chase the tiger then the tiger needs the dog.
((("someone" "is" "big" "+") ("someone" "chases" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If someone chases the squirrel then they see the tiger.
((("someone" "chases" "squirrel" "+")) -> ("someone" "sees" "tiger" "+"))
If someone needs the tiger and they chase the cow then the tiger chases the squirrel.
((("someone" "needs" "tiger" "+") ("someone" "chases" "cow" "+")) -> ("tiger" "chases" "squirrel" "+"))
The squirrel is green.
True
1
proof
[(triple8)]
("squirrel" "is" "green" "+")
triple8
The tiger does not need the cow.
False
1
inv-proof
[(triple13)]
("tiger" "needs" "cow" "-")
triple13
The dog is round.
True
3
proof
[(((triple4 triple5) -> rule3))]
("dog" "is" "round" "+")
((triple4 triple5) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog does not see the tiger.
False
2
inv-proof
[(((triple4) -> rule7))]
("dog" "sees" "tiger" "-")
((triple4) -> (rule7 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger chases the squirrel.
True
4
proof
[(((triple9 ((triple11) -> rule5)) -> rule8))]
("tiger" "chases" "squirrel" "+")
((triple9 ((triple11) -> (rule5 % int2))) -> (rule8 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The dog does not chase the cow.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule5))]
("dog" "chases" "cow" "-")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger sees the tiger.
True
5
proof
[(((((triple9 ((triple11) -> rule5)) -> rule8)) -> rule7))]
("tiger" "sees" "tiger" "+")
((((triple9 ((triple11) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int3
The tiger does not see the tiger.
False
5
inv-proof
[(((((triple9 ((triple11) -> rule5)) -> rule8)) -> rule7))]
("tiger" "sees" "tiger" "-")
((((triple9 ((triple11) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int3
The tiger does not need the dog.
Unknown
inv-rconc
[@1: The tiger needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "needs" "dog" "-")
The cow is green.
Unknown
rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "green" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "round" "-")
The cow chases the squirrel.
Unknown
rconc
[@1: The cow chases the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "squirrel" "+")
The dog does not see the cow.
Unknown
inv-random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The cow needs the squirrel.[(triple1)] The cow needs the tiger.[(triple2)] The cow sees the dog.[(triple3)] The dog chases the squirrel.[(triple4)] The dog is big.[(triple5)] The dog needs the squirrel.[(triple6)] The squirrel is blue.[(triple7)] The squirrel is green.[(triple8)] The squirrel needs the tiger.[(triple9)] The squirrel sees the dog.[(triple10)] The squirrel sees the tiger.[(triple11)] The tiger chases the cow.[(triple12 OR ((((((triple9 ((triple11) -> rule5)) -> rule8)) -> rule7)) -> rule5))] The tiger needs the cow.[(triple13)] The tiger needs the squirrel.[(triple14)] The tiger sees the dog.[(triple15)] @1: The dog is round.[(((triple4 triple5) -> rule3))] The dog sees the tiger.[(((triple4) -> rule7))] The squirrel chases the cow.[(((triple11) -> rule5))] @2: The dog chases the cow.[(((((triple4) -> rule7)) -> rule5))] The tiger chases the squirrel.[(((triple9 ((triple11) -> rule5)) -> rule8))] @3: The tiger sees the tiger.[(((((triple9 ((triple11) -> rule5)) -> rule8)) -> rule7))]
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple6
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple9
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple10
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple11
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple12
((((((triple9 ((triple11) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple13
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The dog is round.
("dog" "is" "round" "+")
((triple4 triple5) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple4) -> (rule7 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
((triple11) -> (rule5 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple9 ((triple11) -> (rule5 % int2))) -> (rule8 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple9 ((triple11) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int3