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