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