The cow eats the tiger. The cow is green. The cow is kind. The cow is nice. The cow is red. The cow is rough. The cow sees the tiger. The cow visits the tiger. The tiger eats the cow. The tiger is green. The tiger is kind. The tiger is nice. The tiger is red. The tiger is rough. The tiger sees the cow. The tiger visits the cow. If something is kind then it eats the cow.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something is kind then it eats the cow.
((("something" "is" "kind" "+")) -> ("something" "eats" "cow" "+"))
The tiger visits the cow.
True
1
proof
[(triple16)]
("tiger" "visits" "cow" "+")
triple16
The cow is not red.
False
1
inv-proof
[(triple5)]
("cow" "is" "red" "-")
triple5
The cow eats the cow.
True
2
proof
[(((triple3) -> rule1))]
("cow" "eats" "cow" "+")
((triple3) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "eats" "cow" "-")
((triple3) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
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 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 visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "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 eats the tiger.[(triple1)] The cow is green.[(triple2)] The cow is kind.[(triple3)] The cow is nice.[(triple4)] The cow is red.[(triple5)] The cow is rough.[(triple6)] The cow sees the tiger.[(triple7)] The cow visits the tiger.[(triple8)] The tiger eats the cow.[(triple9 OR ((triple11) -> rule1))] The tiger is green.[(triple10)] The tiger is kind.[(triple11)] The tiger is nice.[(triple12)] The tiger is red.[(triple13)] The tiger is rough.[(triple14)] The tiger sees the cow.[(triple15)] The tiger visits the cow.[(triple16)] @1: The cow eats the cow.[(((triple3) -> rule1))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
The cow is rough.
("cow" "is" "rough" "+")
triple6
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple7
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple8
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple9
((triple11) -> (rule1 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple16
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple3) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1