The cow chases the tiger. The cow eats the tiger. The cow is big. The cow is cold. The cow is not green. The cow is nice. The cow is young. The cow likes the tiger. The tiger chases the cow. The tiger eats the cow. The tiger is big. The tiger is cold. The tiger is nice. The tiger is young. The tiger does not like the cow. If something is green then it does not like the tiger. If the tiger is cold and the tiger chases the cow then the tiger is green. If something is young and it likes the tiger then it does not like the cow.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow eats the tiger.
("cow" "eats" "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 nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
If something is green then it does not like the tiger.
((("something" "is" "green" "+")) -> ("something" "likes" "tiger" "-"))
If the tiger is cold and the tiger chases the cow then the tiger is green.
((("tiger" "is" "cold" "+") ("tiger" "chases" "cow" "+")) -> ("tiger" "is" "green" "+"))
If something is young and it likes the tiger then it does not like the cow.
((("something" "is" "young" "+") ("something" "likes" "tiger" "+")) -> ("something" "likes" "cow" "-"))
The cow is big.
True
1
proof
[(triple3)]
("cow" "is" "big" "+")
triple3
The tiger likes the cow.
False
1
inv-proof
[(triple15)]
("tiger" "likes" "cow" "+")
triple15
The tiger is green.
True
3
proof
[(((triple12 triple9) -> rule2))]
("tiger" "is" "green" "+")
((triple12 triple9) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
3
inv-proof
[(((triple12 triple9) -> rule2))]
("tiger" "is" "green" "-")
((triple12 triple9) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger does not like the tiger.
True
4
proof
[(((((triple12 triple9) -> rule2)) -> rule1))]
("tiger" "likes" "tiger" "-")
((((triple12 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger likes the tiger.
False
4
inv-proof
[(((((triple12 triple9) -> rule2)) -> rule1))]
("tiger" "likes" "tiger" "+")
((((triple12 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow chases the tiger.[(triple1)] The cow eats the tiger.[(triple2)] The cow is big.[(triple3)] The cow is cold.[(triple4)] The cow is nice.[(triple6)] The cow is not green.[(triple5)] The cow is young.[(triple7)] The cow likes the tiger.[(triple8)] The tiger chases the cow.[(triple9)] The tiger does not like the cow.[(triple15)] The tiger eats the cow.[(triple10)] The tiger is big.[(triple11)] The tiger is cold.[(triple12)] The tiger is nice.[(triple13)] The tiger is young.[(triple14)] @1: The cow does not like the cow.[(((triple7 triple8) -> rule3))] The tiger is green.[(((triple12 triple9) -> rule2))] @2: The tiger does not like the tiger.[(((((triple12 triple9) -> rule2)) -> rule1))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple6
The cow is not green.
("cow" "is" "green" "-")
triple5
The cow is young.
("cow" "is" "young" "+")
triple7
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple8
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple9
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
triple15
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The cow does not like the cow.
("cow" "likes" "cow" "-")
((triple7 triple8) -> (rule3 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple12 triple9) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
((((triple12 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2