The cow eats the tiger. The cow is nice. The cow is round. The cow visits the tiger. The tiger eats the cow. The tiger is green. The tiger is kind. The tiger is nice. The tiger sees the cow. The tiger visits the cow. If something visits the cow and the cow sees the tiger then it visits the tiger. If something eats the cow then the cow sees the tiger.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
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 sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something visits the cow and the cow sees the tiger then it visits the tiger.
((("something" "visits" "cow" "+") ("cow" "sees" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If something eats the cow then the cow sees the tiger.
((("something" "eats" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple8)]
("tiger" "is" "nice" "+")
triple8
The tiger does not visit the cow.
False
1
inv-proof
[(triple10)]
("tiger" "visits" "cow" "-")
triple10
The cow sees the tiger.
True
2
proof
[(((triple5) -> rule2))]
("cow" "sees" "tiger" "+")
((triple5) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not see the tiger.
False
2
inv-proof
[(((triple5) -> rule2))]
("cow" "sees" "tiger" "-")
((triple5) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The tiger visits the tiger.
True
4
proof
[(((triple10 ((triple5) -> rule2)) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple10 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger does not visit the tiger.
False
4
inv-proof
[(((triple10 ((triple5) -> rule2)) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple10 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
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 eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The cow eats the tiger.[(triple1)] The cow is nice.[(triple2)] The cow is round.[(triple3)] The cow visits the tiger.[(triple4)] The tiger eats the cow.[(triple5)] The tiger is green.[(triple6)] The tiger is kind.[(triple7)] The tiger is nice.[(triple8)] The tiger sees the cow.[(triple9)] The tiger visits the cow.[(triple10)] @1: The cow sees the tiger.[(((triple5) -> rule2))] @2: The tiger visits the tiger.[(((triple10 ((triple5) -> rule2)) -> rule1))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple4
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple9
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple5) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple10 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2