The cow is round. The lion needs the cow. The mouse eats the lion. If someone likes the lion then the lion eats the mouse. If the mouse likes the cow and the mouse needs the cow then the mouse eats the cow. If someone eats the cow then the cow likes the lion. If someone needs the cow then they eat the cow. If someone needs the cow and the cow is rough then the cow is big. If someone likes the lion then the lion needs the cow. All young people are not round. If someone eats the lion then they are rough.
The cow is round.
("cow" "is" "round" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
If someone likes the lion then the lion eats the mouse.
((("someone" "likes" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
If the mouse likes the cow and the mouse needs the cow then the mouse eats the cow.
((("mouse" "likes" "cow" "+") ("mouse" "needs" "cow" "+")) -> ("mouse" "eats" "cow" "+"))
If someone eats the cow then the cow likes the lion.
((("someone" "eats" "cow" "+")) -> ("cow" "likes" "lion" "+"))
If someone needs the cow then they eat the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone needs the cow and the cow is rough then the cow is big.
((("someone" "needs" "cow" "+") ("cow" "is" "rough" "+")) -> ("cow" "is" "big" "+"))
If someone likes the lion then the lion needs the cow.
((("someone" "likes" "lion" "+")) -> ("lion" "needs" "cow" "+"))
All young people are not round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "-"))
If someone eats the lion then they are rough.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "rough" "+"))
The mouse eats the lion.
True
1
proof
[(triple3)]
("mouse" "eats" "lion" "+")
triple3
The lion does not need the cow.
False
1
inv-proof
[(triple2)]
("lion" "needs" "cow" "-")
triple2
The mouse is rough.
True
2
proof
[(((triple3) -> rule8))]
("mouse" "is" "rough" "+")
((triple3) -> (rule8 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The lion does not eat the cow.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "eats" "cow" "-")
((triple2) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The cow likes the lion.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("cow" "likes" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("cow" "likes" "lion" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion eats the mouse.
True
4
proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule1))]
("lion" "eats" "mouse" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
The lion does not eat the mouse.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule1))]
("lion" "eats" "mouse" "-")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3
The mouse does not eat the cow.
Unknown
inv-rconc
[@1: The mouse eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "cow" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "rough" "+")
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 eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "+")
The lion does not need the mouse.
Unknown
inv-random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse needs the cow.
Unknown
random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "+")
@0: The cow is round.[(triple1)] The lion needs the cow.[(triple2)] The mouse eats the lion.[(triple3)] @1: The lion eats the cow.[(((triple2) -> rule4))] The mouse is rough.[(((triple3) -> rule8))] @2: The cow likes the lion.[(((((triple2) -> rule4)) -> rule3))] @3: The lion eats the mouse.[(((((((triple2) -> rule4)) -> rule3)) -> rule1))]
The cow is round.
("cow" "is" "round" "+")
triple1
The lion needs the cow.
("lion" "needs" "cow" "+")
triple2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple3
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple2) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3) -> (rule8 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The lion eats the cow.
("lion" "eats" "cow" "+")
int3