The cat does not need the cow. The cat sees the cow. The cow is cold. The cow is red. The cow likes the cat. The cow needs the cat. The cow needs the tiger. The cow sees the tiger. The tiger is blue. The tiger is cold. The tiger is nice. The tiger likes the cat. The tiger likes the cow. The tiger needs the cat. The tiger sees the cat. If someone needs the cat then the cat needs the tiger.
The cat does not need the cow.
("cat" "needs" "cow" "-")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone needs the cat then the cat needs the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple11)]
("tiger" "is" "nice" "+")
triple11
The cow does not like the cat.
False
1
inv-proof
[(triple5)]
("cow" "likes" "cat" "-")
triple5
The cat needs the tiger.
True
2
proof
[(((triple14) -> rule1) OR ((triple6) -> rule1))]
("cat" "needs" "tiger" "+")
((triple14) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple6) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat does not need the tiger.
False
2
inv-proof
[(((triple14) -> rule1) OR ((triple6) -> rule1))]
("cat" "needs" "tiger" "-")
((triple14) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple6) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not see the cow.
Unknown
inv-random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat does not need the cow.[(triple1)] The cat sees the cow.[(triple2)] The cow is cold.[(triple3)] The cow is red.[(triple4)] The cow likes the cat.[(triple5)] The cow needs the cat.[(triple6)] The cow needs the tiger.[(triple7)] The cow sees the tiger.[(triple8)] The tiger is blue.[(triple9)] The tiger is cold.[(triple10)] The tiger is nice.[(triple11)] The tiger likes the cat.[(triple12)] The tiger likes the cow.[(triple13)] The tiger needs the cat.[(triple14)] The tiger sees the cat.[(triple15)] @1: The cat needs the tiger.[(((triple14) -> rule1) OR ((triple6) -> rule1))]
The cat does not need the cow.
("cat" "needs" "cow" "-")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow likes the cat.
("cow" "likes" "cat" "+")
triple5
The cow needs the cat.
("cow" "needs" "cat" "+")
triple6
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple7
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple12
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple13
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple14
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple14) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
((triple6) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1