The cow does not eat the tiger. The cow needs the mouse. The lion eats the cow. The lion is round. The lion needs the cow. The lion does not need the mouse. The mouse eats the cow. The mouse is big. The mouse is not round. The mouse does not need the cow. The mouse does not see the tiger. The tiger eats the cow. The tiger is big. The tiger is young. The tiger needs the lion. If something is young then it eats the mouse. If something sees the cow then it sees the mouse. If something needs the cow then it is not young. If something eats the tiger and it needs the cow then the tiger eats the cow. If something eats the mouse then it sees the cow. If the tiger is not young and the tiger does not see the mouse then the mouse is not green. If something sees the lion and it is not green then the lion needs the tiger. If something needs the tiger and it is big then the tiger is big.
The cow does not eat the tiger.
("cow" "eats" "tiger" "-")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something is young then it eats the mouse.
((("something" "is" "young" "+")) -> ("something" "eats" "mouse" "+"))
If something sees the cow then it sees the mouse.
((("something" "sees" "cow" "+")) -> ("something" "sees" "mouse" "+"))
If something needs the cow then it is not young.
((("something" "needs" "cow" "+")) -> ("something" "is" "young" "-"))
If something eats the tiger and it needs the cow then the tiger eats the cow.
((("something" "eats" "tiger" "+") ("something" "needs" "cow" "+")) -> ("tiger" "eats" "cow" "+"))
If something eats the mouse then it sees the cow.
((("something" "eats" "mouse" "+")) -> ("something" "sees" "cow" "+"))
If the tiger is not young and the tiger does not see the mouse then the mouse is not green.
((("tiger" "is" "young" "~") ("tiger" "sees" "mouse" "~")) -> ("mouse" "is" "green" "-"))
If something sees the lion and it is not green then the lion needs the tiger.
((("something" "sees" "lion" "+") ("something" "is" "green" "~")) -> ("lion" "needs" "tiger" "+"))
If something needs the tiger and it is big then the tiger is big.
((("something" "needs" "tiger" "+") ("something" "is" "big" "+")) -> ("tiger" "is" "big" "+"))
The tiger is young.
True
1
proof
[(triple14)]
("tiger" "is" "young" "+")
triple14
The cow does not need the mouse.
False
1
inv-proof
[(triple2)]
("cow" "needs" "mouse" "-")
triple2
The lion is not young.
True
2
proof
[(((triple5) -> rule3))]
("lion" "is" "young" "-")
((triple5) -> (rule3 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The tiger does not eat the mouse.
False
2
inv-proof
[(((triple14) -> rule1))]
("tiger" "eats" "mouse" "-")
((triple14) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger sees the cow.
True
3
proof
[(((((triple14) -> rule1)) -> rule5))]
("tiger" "sees" "cow" "+")
((((triple14) -> (rule1 % int2))) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger does not see the cow.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule5))]
("tiger" "sees" "cow" "-")
((((triple14) -> (rule1 % int2))) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger sees the mouse.
True
4
proof
[(((((((triple14) -> rule1)) -> rule5)) -> rule2))]
("tiger" "sees" "mouse" "+")
((((((triple14) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The tiger does not see the mouse.
False
4
inv-proof
[(((((((triple14) -> rule1)) -> rule5)) -> rule2))]
("tiger" "sees" "mouse" "-")
((((((triple14) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The lion does not eat the mouse.
Unknown
inv-rconc
[@1: The lion eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "mouse" "-")
The cow sees the cow.
Unknown
rconc
[@2: The cow sees the cow.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cow" "sees" "cow" "+")
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse sees the cow.
Unknown
rconc
[@2: The mouse sees the cow.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "sees" "cow" "+")
The tiger does not eat the lion.
Unknown
inv-random
[@0: The tiger eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "lion" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The cow does not see the lion.
Unknown
inv-random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
@0: The cow does not eat the tiger.[(triple1)] The cow needs the mouse.[(triple2)] The lion does not need the mouse.[(triple6)] The lion eats the cow.[(triple3)] The lion is round.[(triple4)] The lion needs the cow.[(triple5)] The mouse does not need the cow.[(triple10)] The mouse does not see the tiger.[(triple11)] The mouse eats the cow.[(triple7)] The mouse is big.[(triple8)] The mouse is not round.[(triple9)] The tiger eats the cow.[(triple12)] The tiger is big.[(triple13)] The tiger is young.[(triple14)] The tiger needs the lion.[(triple15)] @1: The lion is not young.[(((triple5) -> rule3))] The tiger eats the mouse.[(((triple14) -> rule1))] @2: The tiger sees the cow.[(((((triple14) -> rule1)) -> rule5))] @3: The tiger sees the mouse.[(((((((triple14) -> rule1)) -> rule5)) -> rule2))]
The cow does not eat the tiger.
("cow" "eats" "tiger" "-")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
triple6
The lion eats the cow.
("lion" "eats" "cow" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion needs the cow.
("lion" "needs" "cow" "+")
triple5
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
triple10
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
triple11
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse is not round.
("mouse" "is" "round" "-")
triple9
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple15
The lion is not young.
("lion" "is" "young" "-")
((triple5) -> (rule3 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple14) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((((triple14) -> (rule1 % int2))) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((((((triple14) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3