The cat likes the tiger. The cow likes the mouse. The mouse eats the cow. The mouse is cold. The mouse sees the cat. The mouse sees the tiger. The tiger likes the cat. If the cow is round then the cow likes the mouse. If someone sees the mouse and the mouse eats the cow then they eat the mouse. If someone sees the cat and they like the cat then they see the tiger. If someone eats the mouse then the mouse likes the cat. If someone sees the cat then the cat eats the tiger. If someone eats the tiger then the tiger sees the mouse.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If the cow is round then the cow likes the mouse.
((("cow" "is" "round" "+")) -> ("cow" "likes" "mouse" "+"))
If someone sees the mouse and the mouse eats the cow then they eat the mouse.
((("someone" "sees" "mouse" "+") ("mouse" "eats" "cow" "+")) -> ("someone" "eats" "mouse" "+"))
If someone sees the cat and they like the cat then they see the tiger.
((("someone" "sees" "cat" "+") ("someone" "likes" "cat" "+")) -> ("someone" "sees" "tiger" "+"))
If someone eats the mouse then the mouse likes the cat.
((("someone" "eats" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
If someone sees the cat then the cat eats the tiger.
((("someone" "sees" "cat" "+")) -> ("cat" "eats" "tiger" "+"))
If someone eats the tiger then the tiger sees the mouse.
((("someone" "eats" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
The cow likes the mouse.
True
1
proof
[(triple2)]
("cow" "likes" "mouse" "+")
triple2
The cat does not like the tiger.
False
1
inv-proof
[(triple1)]
("cat" "likes" "tiger" "-")
triple1
The cat eats the tiger.
True
2
proof
[(((triple5) -> rule5))]
("cat" "eats" "tiger" "+")
((triple5) -> (rule5 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat does not eat the tiger.
False
2
inv-proof
[(((triple5) -> rule5))]
("cat" "eats" "tiger" "-")
((triple5) -> (rule5 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The tiger sees the mouse.
True
3
proof
[(((((triple5) -> rule5)) -> rule6))]
("tiger" "sees" "mouse" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The tiger does not see the mouse.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule6))]
("tiger" "sees" "mouse" "-")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The tiger eats the mouse.
True
5
proof
[(((((((triple5) -> rule5)) -> rule6) triple3) -> rule2))]
("tiger" "eats" "mouse" "+")
((((((triple5) -> (rule5 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int3
The tiger does not eat the mouse.
False
5
inv-proof
[(((((((triple5) -> rule5)) -> rule6) triple3) -> rule2))]
("tiger" "eats" "mouse" "-")
((((((triple5) -> (rule5 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int3
The cat does not eat the mouse.
Unknown
inv-rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "mouse" "-")
The cat sees the tiger.
Unknown
rconc
[@1: The cat sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The cow sees the tiger.
Unknown
rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "tiger" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The tiger eats the cat.
Unknown
random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "+")
@0: The cat likes the tiger.[(triple1)] The cow likes the mouse.[(triple2)] The mouse eats the cow.[(triple3)] The mouse is cold.[(triple4)] The mouse sees the cat.[(triple5)] The mouse sees the tiger.[(triple6 OR ((triple5 ((((((((triple5) -> rule5)) -> rule6) triple3) -> rule2)) -> rule4)) -> rule3))] The tiger likes the cat.[(triple7)] @1: The cat eats the tiger.[(((triple5) -> rule5))] @2: The tiger sees the mouse.[(((((triple5) -> rule5)) -> rule6))] @3: The tiger eats the mouse.[(((((((triple5) -> rule5)) -> rule6) triple3) -> rule2))] @4: The mouse likes the cat.[(((((((((triple5) -> rule5)) -> rule6) triple3) -> rule2)) -> rule4))]
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
((triple5 ((((((((triple5) -> (rule5 % int5))) -> (rule6 % int4)) triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int4
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int5
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
The cat eats the tiger.
("cat" "eats" "tiger" "+")
((triple5) -> (rule5 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((((triple5) -> (rule5 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((((((((triple5) -> (rule5 % int4))) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int4