The cow is big. The lion eats the tiger. The lion is blue. The mouse eats the cow. The mouse is red. The tiger is green. The tiger likes the lion. If someone is big then they need the mouse. If the lion is green then the lion eats the cow. If someone likes the cow and the cow eats the mouse then the cow is kind. If someone eats the cow and the cow likes the lion then the cow likes the tiger. If someone needs the mouse then they eat the lion. Big people are blue. Blue people are red. If someone needs the mouse then they need the tiger. If someone needs the tiger then the tiger is big.
The cow is big.
("cow" "is" "big" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is red.
("mouse" "is" "red" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If someone is big then they need the mouse.
((("someone" "is" "big" "+")) -> ("someone" "needs" "mouse" "+"))
If the lion is green then the lion eats the cow.
((("lion" "is" "green" "+")) -> ("lion" "eats" "cow" "+"))
If someone likes the cow and the cow eats the mouse then the cow is kind.
((("someone" "likes" "cow" "+") ("cow" "eats" "mouse" "+")) -> ("cow" "is" "kind" "+"))
If someone eats the cow and the cow likes the lion then the cow likes the tiger.
((("someone" "eats" "cow" "+") ("cow" "likes" "lion" "+")) -> ("cow" "likes" "tiger" "+"))
If someone needs the mouse then they eat the lion.
((("someone" "needs" "mouse" "+")) -> ("someone" "eats" "lion" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone needs the mouse then they need the tiger.
((("someone" "needs" "mouse" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the tiger then the tiger is big.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "big" "+"))
The lion is blue.
True
1
proof
[(triple3)]
("lion" "is" "blue" "+")
triple3
The lion does not eat the tiger.
False
1
inv-proof
[(triple2)]
("lion" "eats" "tiger" "-")
triple2
The cow is blue.
True
2
proof
[(((triple1) -> rule6))]
("cow" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "is" "blue" "-")
((triple1) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("cow" "needs" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow does not need the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("cow" "needs" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The tiger is big.
True
4
proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule9))]
("tiger" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The tiger is not big.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule9))]
("tiger" "is" "big" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The tiger needs the mouse.
True
5
proof
[(((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule1))]
("tiger" "needs" "mouse" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The tiger is not blue.
False
5
inv-proof
[(((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule6))]
("tiger" "is" "blue" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The tiger needs the tiger.
True
6
proof
[(((((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule1)) -> rule8))]
("tiger" "needs" "tiger" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5
The tiger is not red.
False
6
inv-proof
[(((((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule6)) -> rule7))]
("tiger" "is" "red" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5
The lion does not need the tiger.
Unknown
inv-rconc
[@2: The lion needs the tiger.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("lion" "needs" "tiger" "-")
The mouse eats the lion.
Unknown
rconc
[@2: The mouse eats the lion.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "eats" "lion" "+")
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "kind" "-")
The mouse needs the tiger.
Unknown
rconc
[@2: The mouse needs the tiger.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("mouse" "needs" "tiger" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@2: The lion eats the lion.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("lion" "eats" "lion" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "blue" "+")
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The tiger does not need the lion.
Unknown
inv-random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "-")
The mouse needs the cow.
Unknown
random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "+")
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 cow eats the tiger.
Unknown
random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "+")
@0: The cow is big.[(triple1)] The lion eats the tiger.[(triple2)] The lion is blue.[(triple3)] The mouse eats the cow.[(triple4)] The mouse is red.[(triple5)] The tiger is green.[(triple6)] The tiger likes the lion.[(triple7)] @1: The cow is blue.[(((triple1) -> rule6))] The cow needs the mouse.[(((triple1) -> rule1))] The lion is red.[(((triple3) -> rule7))] @2: The cow eats the lion.[(((((triple1) -> rule1)) -> rule5))] The cow is red.[(((((triple1) -> rule6)) -> rule7))] The cow needs the tiger.[(((((triple1) -> rule1)) -> rule8))] @3: The tiger is big.[(((((((triple1) -> rule1)) -> rule8)) -> rule9))] @4: The tiger is blue.[(((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule6))] The tiger needs the mouse.[(((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule1))] @5: The tiger eats the lion.[(((((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule1)) -> rule5))] The tiger is red.[(((((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule6)) -> rule7))] The tiger needs the tiger.[(((((((((((triple1) -> rule1)) -> rule8)) -> rule9)) -> rule1)) -> rule8))]
The cow is big.
("cow" "is" "big" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple7
The cow is blue.
("cow" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple1) -> (rule1 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple3) -> (rule7 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int4
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5
The tiger is red.
("tiger" "is" "red" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int5