The bear eats the mouse. The bear eats the tiger. The lion sees the bear. The lion sees the mouse. The lion sees the tiger. The mouse does not like the bear. The tiger sees the mouse. If the lion eats the bear and the bear is not young then the bear likes the lion. If the tiger sees the mouse and the mouse eats the tiger then the mouse likes the lion. If something likes the mouse then the mouse eats the tiger. If something likes the tiger then the tiger is red. If something eats the bear then the bear likes the mouse. If the mouse sees the bear and the mouse is not big then the mouse is rough. If something is green then it does not like the mouse. If something likes the lion then the lion eats the bear. If the lion sees the mouse then the mouse eats the bear.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the lion eats the bear and the bear is not young then the bear likes the lion.
((("lion" "eats" "bear" "+") ("bear" "is" "young" "~")) -> ("bear" "likes" "lion" "+"))
If the tiger sees the mouse and the mouse eats the tiger then the mouse likes the lion.
((("tiger" "sees" "mouse" "+") ("mouse" "eats" "tiger" "+")) -> ("mouse" "likes" "lion" "+"))
If something likes the mouse then the mouse eats the tiger.
((("something" "likes" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If something likes the tiger then the tiger is red.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something eats the bear then the bear likes the mouse.
((("something" "eats" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If the mouse sees the bear and the mouse is not big then the mouse is rough.
((("mouse" "sees" "bear" "+") ("mouse" "is" "big" "~")) -> ("mouse" "is" "rough" "+"))
If something is green then it does not like the mouse.
((("something" "is" "green" "+")) -> ("something" "likes" "mouse" "-"))
If something likes the lion then the lion eats the bear.
((("something" "likes" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If the lion sees the mouse then the mouse eats the bear.
((("lion" "sees" "mouse" "+")) -> ("mouse" "eats" "bear" "+"))
The lion sees the bear.
True
1
proof
[(triple3)]
("lion" "sees" "bear" "+")
triple3
The tiger does not see the mouse.
False
1
inv-proof
[(triple7)]
("tiger" "sees" "mouse" "-")
triple7
The mouse eats the bear.
True
2
proof
[(((triple4) -> rule9))]
("mouse" "eats" "bear" "+")
((triple4) -> (rule9 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not eat the bear.
False
2
inv-proof
[(((triple4) -> rule9))]
("mouse" "eats" "bear" "-")
((triple4) -> (rule9 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The bear likes the mouse.
True
3
proof
[(((((triple4) -> rule9)) -> rule5))]
("bear" "likes" "mouse" "+")
((((triple4) -> (rule9 % int2))) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The bear does not like the mouse.
False
3
inv-proof
[(((((triple4) -> rule9)) -> rule5))]
("bear" "likes" "mouse" "-")
((((triple4) -> (rule9 % int2))) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The mouse eats the tiger.
True
4
proof
[(((((((triple4) -> rule9)) -> rule5)) -> rule3))]
("mouse" "eats" "tiger" "+")
((((((triple4) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The mouse does not eat the tiger.
False
4
inv-proof
[(((((((triple4) -> rule9)) -> rule5)) -> rule3))]
("mouse" "eats" "tiger" "-")
((((((triple4) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The mouse likes the lion.
True
6
proof
[(((triple7 ((((((triple4) -> rule9)) -> rule5)) -> rule3)) -> rule2))]
("mouse" "likes" "lion" "+")
((triple7 ((((((triple4) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int4
The mouse does not like the lion.
False
6
inv-proof
[(((triple7 ((((((triple4) -> rule9)) -> rule5)) -> rule3)) -> rule2))]
("mouse" "likes" "lion" "-")
((triple7 ((((((triple4) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int4
The lion eats the bear.
True
7
proof
[(((((triple7 ((((((triple4) -> rule9)) -> rule5)) -> rule3)) -> rule2)) -> rule8))]
("lion" "eats" "bear" "+")
((((triple7 ((((((triple4) -> (rule9 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int5
The lion does not eat the bear.
False
7
inv-proof
[(((((triple7 ((((((triple4) -> rule9)) -> rule5)) -> rule3)) -> rule2)) -> rule8))]
("lion" "eats" "bear" "-")
((((triple7 ((((((triple4) -> (rule9 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int5
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "red" "-")
The bear likes the lion.
Unknown
rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "lion" "+")
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "rough" "-")
The bear eats the lion.
Unknown
random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The tiger likes the lion.
Unknown
random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "+")
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The lion likes the bear.
Unknown
random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "+")
@0: The bear eats the mouse.[(triple1)] The bear eats the tiger.[(triple2)] The lion sees the bear.[(triple3)] The lion sees the mouse.[(triple4)] The lion sees the tiger.[(triple5)] The mouse does not like the bear.[(triple6)] The tiger sees the mouse.[(triple7)] @1: The mouse eats the bear.[(((triple4) -> rule9))] @2: The bear likes the mouse.[(((((triple4) -> rule9)) -> rule5))] @3: The mouse eats the tiger.[(((((((triple4) -> rule9)) -> rule5)) -> rule3))] @4: The mouse likes the lion.[(((triple7 ((((((triple4) -> rule9)) -> rule5)) -> rule3)) -> rule2))] @5: The lion eats the bear.[(((((triple7 ((((((triple4) -> rule9)) -> rule5)) -> rule3)) -> rule2)) -> rule8))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The lion sees the bear.
("lion" "sees" "bear" "+")
triple3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple5
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple4) -> (rule9 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((((triple4) -> (rule9 % int2))) -> (rule5 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((((((triple4) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple7 ((((((triple4) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int4
The lion eats the bear.
("lion" "eats" "bear" "+")
((((triple7 ((((((triple4) -> (rule9 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int5