The cow does not chase the lion. The cow eats the rabbit. The cow is young. The lion eats the tiger. The rabbit is green. The rabbit needs the cow. The rabbit does not need the lion. The tiger chases the cow. The tiger does not eat the rabbit. The tiger is not green. The tiger needs the rabbit. If the lion chases the rabbit then the lion does not eat the tiger. If something is cold then it eats the cow. If the tiger is big then the tiger is not young. If something is round then it eats the lion. If something eats the cow and it eats the rabbit then it is green. If something eats the lion and it eats the tiger then the lion does not need the cow. If something needs the cow then the cow needs the tiger. If something needs the tiger then the tiger is cold. If something eats the tiger and the tiger eats the cow then the tiger is big.
The cow does not chase the lion.
("cow" "chases" "lion" "-")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is young.
("cow" "is" "young" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If the lion chases the rabbit then the lion does not eat the tiger.
((("lion" "chases" "rabbit" "+")) -> ("lion" "eats" "tiger" "-"))
If something is cold then it eats the cow.
((("something" "is" "cold" "+")) -> ("something" "eats" "cow" "+"))
If the tiger is big then the tiger is not young.
((("tiger" "is" "big" "+")) -> ("tiger" "is" "young" "-"))
If something is round then it eats the lion.
((("something" "is" "round" "+")) -> ("something" "eats" "lion" "+"))
If something eats the cow and it eats the rabbit then it is green.
((("something" "eats" "cow" "+") ("something" "eats" "rabbit" "+")) -> ("something" "is" "green" "+"))
If something eats the lion and it eats the tiger then the lion does not need the cow.
((("something" "eats" "lion" "+") ("something" "eats" "tiger" "+")) -> ("lion" "needs" "cow" "-"))
If something needs the cow then the cow needs the tiger.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
If something needs the tiger then the tiger is cold.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something eats the tiger and the tiger eats the cow then the tiger is big.
((("something" "eats" "tiger" "+") ("tiger" "eats" "cow" "+")) -> ("tiger" "is" "big" "+"))
The rabbit needs the cow.
True
1
proof
[(triple6)]
("rabbit" "needs" "cow" "+")
triple6
The cow is not young.
False
1
inv-proof
[(triple3)]
("cow" "is" "young" "-")
triple3
The cow needs the tiger.
True
2
proof
[(((triple6) -> rule7))]
("cow" "needs" "tiger" "+")
((triple6) -> (rule7 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow does not need the tiger.
False
2
inv-proof
[(((triple6) -> rule7))]
("cow" "needs" "tiger" "-")
((triple6) -> (rule7 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger is cold.
True
3
proof
[(((((triple6) -> rule7)) -> rule8))]
("tiger" "is" "cold" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The tiger is not cold.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule8))]
("tiger" "is" "cold" "-")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The tiger eats the cow.
True
4
proof
[(((((((triple6) -> rule7)) -> rule8)) -> rule2))]
("tiger" "eats" "cow" "+")
((((((triple6) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The tiger does not eat the cow.
False
4
inv-proof
[(((((((triple6) -> rule7)) -> rule8)) -> rule2))]
("tiger" "eats" "cow" "-")
((((((triple6) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The tiger is big.
True
6
proof
[(((triple4 ((((((triple6) -> rule7)) -> rule8)) -> rule2)) -> rule9))]
("tiger" "is" "big" "+")
((triple4 ((((((triple6) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The tiger is not big.
False
6
inv-proof
[(((triple4 ((((((triple6) -> rule7)) -> rule8)) -> rule2)) -> rule9))]
("tiger" "is" "big" "-")
((triple4 ((((((triple6) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The tiger is not young.
True
7
proof
[(((((triple4 ((((((triple6) -> rule7)) -> rule8)) -> rule2)) -> rule9)) -> rule3))]
("tiger" "is" "young" "-")
((((triple4 ((((((triple6) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int5
The tiger is young.
False
7
inv-proof
[(((((triple4 ((((((triple6) -> rule7)) -> rule8)) -> rule2)) -> rule9)) -> rule3))]
("tiger" "is" "young" "+")
((((triple4 ((((((triple6) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int5
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion eats the cow.
Unknown
rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "cow" "+")
The cow does not eat the lion.
Unknown
inv-rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "lion" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "green" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "lion" "-")
The rabbit eats the cow.
Unknown
rconc
[@1: The rabbit eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "cow" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow does not chase the tiger.
Unknown
inv-random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow chases the rabbit.
Unknown
random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "+")
@0: The cow does not chase the lion.[(triple1)] The cow eats the rabbit.[(triple2)] The cow is young.[(triple3)] The lion eats the tiger.[(triple4)] The rabbit does not need the lion.[(triple7)] The rabbit is green.[(triple5)] The rabbit needs the cow.[(triple6)] The tiger chases the cow.[(triple8)] The tiger does not eat the rabbit.[(triple9)] The tiger is not green.[(triple10)] The tiger needs the rabbit.[(triple11)] @1: The cow needs the tiger.[(((triple6) -> rule7))] @2: The tiger is cold.[(((((triple6) -> rule7)) -> rule8))] @3: The tiger eats the cow.[(((((((triple6) -> rule7)) -> rule8)) -> rule2))] @4: The tiger is big.[(((triple4 ((((((triple6) -> rule7)) -> rule8)) -> rule2)) -> rule9))] @5: The tiger is not young.[(((((triple4 ((((((triple6) -> rule7)) -> rule8)) -> rule2)) -> rule9)) -> rule3))]
The cow does not chase the lion.
("cow" "chases" "lion" "-")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple4
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple6
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger does not eat the rabbit.
("tiger" "eats" "rabbit" "-")
triple9
The tiger is not green.
("tiger" "is" "green" "-")
triple10
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple6) -> (rule7 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
((((((triple6) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
((triple4 ((((((triple6) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int4
The tiger is not young.
("tiger" "is" "young" "-")
((((triple4 ((((((triple6) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is not young.
("tiger" "is" "young" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int5