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