The cat does not chase the cow. The cat chases the mouse. The cat eats the cow. The cat eats the tiger. The cat is rough. The cat is round. The cow chases the mouse. The cow eats the mouse. The cow is round. The mouse chases the cat. The mouse is rough. The tiger is young. The tiger needs the cat. The tiger does not need the cow. If someone chases the tiger and they eat the tiger then they chase the cat. If someone needs the mouse then they are red. If someone chases the mouse then they need the mouse. If someone is round then they eat the tiger. If someone chases the cow then they chase the mouse. If someone needs the mouse then the mouse chases the cow.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is round.
("cow" "is" "round" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
If someone chases the tiger and they eat the tiger then they chase the cat.
((("someone" "chases" "tiger" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "chases" "cat" "+"))
If someone needs the mouse then they are red.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "red" "+"))
If someone chases the mouse then they need the mouse.
((("someone" "chases" "mouse" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is round then they eat the tiger.
((("someone" "is" "round" "+")) -> ("someone" "eats" "tiger" "+"))
If someone chases the cow then they chase the mouse.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "mouse" "+"))
If someone needs the mouse then the mouse chases the cow.
((("someone" "needs" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
The cat is round.
True
1
proof
[(triple6)]
("cat" "is" "round" "+")
triple6
The cat is not rough.
False
1
inv-proof
[(triple5)]
("cat" "is" "rough" "-")
triple5
The cow needs the mouse.
True
2
proof
[(((triple7) -> rule3))]
("cow" "needs" "mouse" "+")
((triple7) -> (rule3 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow does not eat the tiger.
False
2
inv-proof
[(((triple9) -> rule4))]
("cow" "eats" "tiger" "-")
((triple9) -> (rule4 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is red.
True
3
proof
[(((((triple7) -> rule3)) -> rule2))]
("cow" "is" "red" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cat is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("cat" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((triple7) -> rule3)) -> rule6)) -> rule5))]
("mouse" "chases" "mouse" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((triple7) -> rule3)) -> rule6)) -> rule5))]
("mouse" "chases" "mouse" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse needs the mouse.
True
5
proof
[(((((((((triple2) -> rule3)) -> rule6)) -> rule5)) -> rule3) OR ((((((((triple7) -> rule3)) -> rule6)) -> rule5)) -> rule3))]
("mouse" "needs" "mouse" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
((((((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The mouse does not need the mouse.
False
5
inv-proof
[(((((((((triple2) -> rule3)) -> rule6)) -> rule5)) -> rule3) OR ((((((((triple7) -> rule3)) -> rule6)) -> rule5)) -> rule3))]
("mouse" "needs" "mouse" "-")
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
((((((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The mouse is red.
True
6
proof
[(((((((((((triple2) -> rule3)) -> rule6)) -> rule5)) -> rule3)) -> rule2) OR ((((((((((triple7) -> rule3)) -> rule6)) -> rule5)) -> rule3)) -> rule2))]
("mouse" "is" "red" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
((((((((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5
The mouse is not red.
False
6
inv-proof
[(((((((((((triple2) -> rule3)) -> rule6)) -> rule5)) -> rule3)) -> rule2) OR ((((((((((triple7) -> rule3)) -> rule6)) -> rule5)) -> rule3)) -> rule2))]
("mouse" "is" "red" "-")
((((((((((triple2) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
((((((((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5
The tiger does not need the mouse.
Unknown
inv-rconc
[@2: The tiger needs the mouse.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("tiger" "needs" "mouse" "-")
The tiger chases the cat.
Unknown
rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "cat" "+")
The cow does not chase the cat.
Unknown
inv-rconc
[@1: The cow chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cat" "-")
The tiger chases the mouse.
Unknown
rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "mouse" "+")
The mouse does not eat the tiger.
Unknown
inv-rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "tiger" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The cow does not need the tiger.
Unknown
inv-random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "-")
The mouse eats the cow.
Unknown
random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "+")
The tiger does not chase the cow.
Unknown
inv-random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cat chases the mouse.[(triple2)] The cat does not chase the cow.[(triple1)] The cat eats the cow.[(triple3)] The cat eats the tiger.[(triple4 OR ((triple6) -> rule4))] The cat is rough.[(triple5)] The cat is round.[(triple6)] The cow chases the mouse.[(triple7)] The cow eats the mouse.[(triple8)] The cow is round.[(triple9)] The mouse chases the cat.[(triple10)] The mouse is rough.[(triple11)] The tiger does not need the cow.[(triple14)] The tiger is young.[(triple12)] The tiger needs the cat.[(triple13)] @1: The cat needs the mouse.[(((triple2) -> rule3))] The cow eats the tiger.[(((triple9) -> rule4))] The cow needs the mouse.[(((triple7) -> rule3))] @2: The cat is red.[(((((triple2) -> rule3)) -> rule2))] The cow is red.[(((((triple7) -> rule3)) -> rule2))] The mouse chases the cow.[(((((triple2) -> rule3)) -> rule6) OR ((((triple7) -> rule3)) -> rule6))] @3: The mouse chases the mouse.[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((triple7) -> rule3)) -> rule6)) -> rule5))] @4: The mouse needs the mouse.[(((((((((triple2) -> rule3)) -> rule6)) -> rule5)) -> rule3) OR ((((((((triple7) -> rule3)) -> rule6)) -> rule5)) -> rule3))] @5: The mouse is red.[(((((((((((triple2) -> rule3)) -> rule6)) -> rule5)) -> rule3)) -> rule2) OR ((((((((((triple7) -> rule3)) -> rule6)) -> rule5)) -> rule3)) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple3
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple4
((triple6) -> (rule4 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple7
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple8
The cow is round.
("cow" "is" "round" "+")
triple9
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple13
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple2) -> (rule3 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((triple9) -> (rule4 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple7) -> (rule3 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
((((((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
((((((((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5