The cat does not need the tiger. The cow is blue. The cow needs the lion. The cow visits the lion. The lion needs the cat. The lion sees the cat. The lion sees the cow. The lion does not see the tiger. The lion visits the cat. The tiger needs the cat. The tiger visits the cat. The tiger visits the lion. If someone visits the cow and they are cold then they do not need the cow. If someone sees the cat then the cat needs the cow.
The cat does not need the tiger.
("cat" "needs" "tiger" "-")
The cow is blue.
("cow" "is" "blue" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
The lion visits the cat.
("lion" "visits" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone visits the cow and they are cold then they do not need the cow.
((("someone" "visits" "cow" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "cow" "-"))
If someone sees the cat then the cat needs the cow.
((("someone" "sees" "cat" "+")) -> ("cat" "needs" "cow" "+"))
The cow is blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
The tiger does not need the cat.
False
1
inv-proof
[(triple10)]
("tiger" "needs" "cat" "-")
triple10
The cat needs the cow.
True
2
proof
[(((triple6) -> rule2))]
("cat" "needs" "cow" "+")
((triple6) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat does not need the cow.
False
2
inv-proof
[(((triple6) -> rule2))]
("cat" "needs" "cow" "-")
((triple6) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The cow does not need the tiger.
Unknown
inv-random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cat does not need the tiger.[(triple1)] The cow is blue.[(triple2)] The cow needs the lion.[(triple3)] The cow visits the lion.[(triple4)] The lion does not see the tiger.[(triple8)] The lion needs the cat.[(triple5)] The lion sees the cat.[(triple6)] The lion sees the cow.[(triple7)] The lion visits the cat.[(triple9)] The tiger needs the cat.[(triple10)] The tiger visits the cat.[(triple11)] The tiger visits the lion.[(triple12)] @1: The cat needs the cow.[(((triple6) -> rule2))]
The cat does not need the tiger.
("cat" "needs" "tiger" "-")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow needs the lion.
("cow" "needs" "lion" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
triple8
The lion needs the cat.
("lion" "needs" "cat" "+")
triple5
The lion sees the cat.
("lion" "sees" "cat" "+")
triple6
The lion sees the cow.
("lion" "sees" "cow" "+")
triple7
The lion visits the cat.
("lion" "visits" "cat" "+")
triple9
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple11
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple12
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple6) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1