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