The cow is blue. The cow is kind. The cow is nice. The cow is red. The cow is young. The cow needs the tiger. The cow sees the tiger. The cow visits the tiger. The tiger is blue. The tiger is kind. The tiger is red. The tiger is young. The tiger needs the cow. The tiger sees the cow. The tiger visits the cow. If someone sees the cow and they need the tiger then the cow sees the tiger. If someone visits the tiger and the tiger needs the cow then they visit the cow. If someone sees the tiger then they see the cow.
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone sees the cow and they need the tiger then the cow sees the tiger.
((("someone" "sees" "cow" "+") ("someone" "needs" "tiger" "+")) -> ("cow" "sees" "tiger" "+"))
If someone visits the tiger and the tiger needs the cow then they visit the cow.
((("someone" "visits" "tiger" "+") ("tiger" "needs" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone sees the tiger then they see the cow.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "cow" "+"))
The tiger is red.
True
1
proof
[(triple11)]
("tiger" "is" "red" "+")
triple11
The cow does not need the tiger.
False
1
inv-proof
[(triple6)]
("cow" "needs" "tiger" "-")
triple6
The cow visits the cow.
True
3
proof
[(((triple8 triple13) -> rule2))]
("cow" "visits" "cow" "+")
((triple8 triple13) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple7) -> rule3))]
("cow" "sees" "cow" "-")
((triple7) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
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 tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
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 nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The cow is blue.[(triple1)] The cow is kind.[(triple2)] The cow is nice.[(triple3)] The cow is red.[(triple4)] The cow is young.[(triple5)] The cow needs the tiger.[(triple6)] The cow sees the tiger.[(triple7)] The cow visits the tiger.[(triple8)] The tiger is blue.[(triple9)] The tiger is kind.[(triple10)] The tiger is red.[(triple11)] The tiger is young.[(triple12)] The tiger needs the cow.[(triple13)] The tiger sees the cow.[(triple14)] The tiger visits the cow.[(triple15)] @1: The cow sees the cow.[(((triple7) -> rule3))] The cow visits the cow.[(((triple8 triple13) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple7
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple13
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple7) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple8 triple13) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1