The cow does not like the lion. The lion likes the cow. The squirrel visits the cow. If someone visits the cow then the cow needs the squirrel. If the cow likes the lion and the cow is not kind then the lion visits the squirrel. If the cow is cold and the cow likes the lion then the cow does not visit the squirrel. If the squirrel needs the cow then the squirrel is blue. If someone likes the lion then the lion is not blue. If the cow needs the lion then the lion is not cold. If someone needs the squirrel then they need the lion. If someone needs the cow then the cow does not like the lion.
The cow does not like the lion.
("cow" "likes" "lion" "-")
The lion likes the cow.
("lion" "likes" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone visits the cow then the cow needs the squirrel.
((("someone" "visits" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
If the cow likes the lion and the cow is not kind then the lion visits the squirrel.
((("cow" "likes" "lion" "+") ("cow" "is" "kind" "~")) -> ("lion" "visits" "squirrel" "+"))
If the cow is cold and the cow likes the lion then the cow does not visit the squirrel.
((("cow" "is" "cold" "+") ("cow" "likes" "lion" "+")) -> ("cow" "visits" "squirrel" "-"))
If the squirrel needs the cow then the squirrel is blue.
((("squirrel" "needs" "cow" "+")) -> ("squirrel" "is" "blue" "+"))
If someone likes the lion then the lion is not blue.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "blue" "-"))
If the cow needs the lion then the lion is not cold.
((("cow" "needs" "lion" "+")) -> ("lion" "is" "cold" "-"))
If someone needs the squirrel then they need the lion.
((("someone" "needs" "squirrel" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the cow then the cow does not like the lion.
((("someone" "needs" "cow" "+")) -> ("cow" "likes" "lion" "-"))
The lion likes the cow.
True
1
proof
[(triple2)]
("lion" "likes" "cow" "+")
triple2
The cow likes the lion.
False
1
inv-proof
[(triple1)]
("cow" "likes" "lion" "+")
triple1
The cow needs the squirrel.
True
2
proof
[(((triple3) -> rule1))]
("cow" "needs" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow does not need the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "needs" "squirrel" "-")
((triple3) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow needs the lion.
True
3
proof
[(((((triple3) -> rule1)) -> rule7))]
("cow" "needs" "lion" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow does not need the lion.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("cow" "needs" "lion" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The lion is not cold.
True
4
proof
[(((((((triple3) -> rule1)) -> rule7)) -> rule6))]
("lion" "is" "cold" "-")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The lion is cold.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule7)) -> rule6))]
("lion" "is" "cold" "+")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel needs the lion.
Unknown
rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "needs" "lion" "+")
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion visits the squirrel.
Unknown
rconc
[@1: The lion visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "squirrel" "+")
The squirrel does not visit the lion.
Unknown
inv-random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "-")
The cow likes the squirrel.
Unknown
random
[@0: The cow likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "squirrel" "+")
The squirrel does not like the lion.
Unknown
inv-random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The cow does not like the lion.[(triple1)] The lion likes the cow.[(triple2)] The squirrel visits the cow.[(triple3)] @1: The cow needs the squirrel.[(((triple3) -> rule1))] @2: The cow needs the lion.[(((((triple3) -> rule1)) -> rule7))] @3: The lion is not cold.[(((((((triple3) -> rule1)) -> rule7)) -> rule6))]
The cow does not like the lion.
("cow" "likes" "lion" "-")
triple1
The lion likes the cow.
("lion" "likes" "cow" "+")
triple2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The lion is not cold.
("lion" "is" "cold" "-")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3