The cat does not visit the cow. The cow needs the tiger. The cow visits the cat. The tiger eats the cat. The tiger is green. The tiger is young. The tiger visits the cow. If something eats the cow then the cow eats the cat. If something needs the tiger then the tiger eats the cow.
The cat does not visit the cow.
("cat" "visits" "cow" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something eats the cow then the cow eats the cat.
((("something" "eats" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If something needs the tiger then the tiger eats the cow.
((("something" "needs" "tiger" "+")) -> ("tiger" "eats" "cow" "+"))
The tiger is green.
True
1
proof
[(triple5)]
("tiger" "is" "green" "+")
triple5
The cow does not visit the cat.
False
1
inv-proof
[(triple3)]
("cow" "visits" "cat" "-")
triple3
The tiger eats the cow.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "eats" "cow" "+")
((triple2) -> (rule2 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger does not eat the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "eats" "cow" "-")
((triple2) -> (rule2 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The cow eats the cat.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "eats" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The cow does not eat the cat.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "eats" "cat" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
The tiger does not visit the cat.
Unknown
inv-random
[@0: The tiger visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cat" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat does not eat the cow.
Unknown
inv-random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cat does not visit the cow.[(triple1)] The cow needs the tiger.[(triple2)] The cow visits the cat.[(triple3)] The tiger eats the cat.[(triple4)] The tiger is green.[(triple5)] The tiger is young.[(triple6)] The tiger visits the cow.[(triple7)] @1: The tiger eats the cow.[(((triple2) -> rule2))] @2: The cow eats the cat.[(((((triple2) -> rule2)) -> rule1))]
The cat does not visit the cow.
("cat" "visits" "cow" "-")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The cow visits the cat.
("cow" "visits" "cat" "+")
triple3
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple4
The tiger is green.
("tiger" "is" "green" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
((triple2) -> (rule2 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2