The cat eats the mouse. The cat is big. The cat is rough. The cat needs the cow. The cow is red. The lion is big. The lion is red. The lion is rough. The lion likes the cat. The lion does not like the cow. The mouse eats the cat. The mouse eats the lion. The mouse is round. The mouse likes the cat. The mouse does not like the lion. The mouse needs the lion. If something eats the cow then the cow does not eat the cat. If something likes the mouse then it is red. If something likes the cat and the cat eats the cow then the cat needs the cow. If something likes the cat then it eats the cow. If the cow is not rough then the cow does not eat the mouse. If something is rough and it does not eat the mouse then it is not blue.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion does not like the cow.
("lion" "likes" "cow" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If something eats the cow then the cow does not eat the cat.
((("something" "eats" "cow" "+")) -> ("cow" "eats" "cat" "-"))
If something likes the mouse then it is red.
((("something" "likes" "mouse" "+")) -> ("something" "is" "red" "+"))
If something likes the cat and the cat eats the cow then the cat needs the cow.
((("something" "likes" "cat" "+") ("cat" "eats" "cow" "+")) -> ("cat" "needs" "cow" "+"))
If something likes the cat then it eats the cow.
((("something" "likes" "cat" "+")) -> ("something" "eats" "cow" "+"))
If the cow is not rough then the cow does not eat the mouse.
((("cow" "is" "rough" "~")) -> ("cow" "eats" "mouse" "-"))
If something is rough and it does not eat the mouse then it is not blue.
((("something" "is" "rough" "+") ("something" "eats" "mouse" "~")) -> ("something" "is" "blue" "-"))
The lion is red.
True
1
proof
[(triple7)]
("lion" "is" "red" "+")
triple7
The mouse likes the lion.
False
1
inv-proof
[(triple15)]
("mouse" "likes" "lion" "+")
triple15
The mouse eats the cow.
True
2
proof
[(((triple14) -> rule4))]
("mouse" "eats" "cow" "+")
((triple14) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The lion does not eat the cow.
False
2
inv-proof
[(((triple9) -> rule4))]
("lion" "eats" "cow" "-")
((triple9) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The cow does not eat the cat.
True
3
proof
[(((((triple14) -> rule4)) -> rule1) OR ((((triple9) -> rule4)) -> rule1))]
("cow" "eats" "cat" "-")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow eats the cat.
False
3
inv-proof
[(((((triple14) -> rule4)) -> rule1) OR ((((triple9) -> rule4)) -> rule1))]
("cow" "eats" "cat" "+")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cat does not eat the cow.
Unknown
inv-rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cow" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "red" "+")
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion needs the mouse.
Unknown
random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "+")
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 rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cat eats the mouse.[(triple1)] The cat is big.[(triple2)] The cat is rough.[(triple3)] The cat needs the cow.[(triple4)] The cow is red.[(triple5)] The lion does not like the cow.[(triple10)] The lion is big.[(triple6)] The lion is red.[(triple7)] The lion is rough.[(triple8)] The lion likes the cat.[(triple9)] The mouse does not like the lion.[(triple15)] The mouse eats the cat.[(triple11)] The mouse eats the lion.[(triple12)] The mouse is round.[(triple13)] The mouse likes the cat.[(triple14)] The mouse needs the lion.[(triple16)] @1: The lion eats the cow.[(((triple9) -> rule4))] The mouse eats the cow.[(((triple14) -> rule4))] @2: The cow does not eat the cat.[(((((triple14) -> rule4)) -> rule1) OR ((((triple9) -> rule4)) -> rule1))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat needs the cow.
("cat" "needs" "cow" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
The lion does not like the cow.
("lion" "likes" "cow" "-")
triple10
The lion is big.
("lion" "is" "big" "+")
triple6
The lion is red.
("lion" "is" "red" "+")
triple7
The lion is rough.
("lion" "is" "rough" "+")
triple8
The lion likes the cat.
("lion" "likes" "cat" "+")
triple9
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
triple15
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple11
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple14
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple16
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple9) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
((triple14) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The cow does not eat the cat.
("cow" "eats" "cat" "-")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2