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