The cow chases the tiger. The cow likes the tiger. The tiger likes the cow. If something chases the tiger then it visits the cow. If something chases the cow then the cow is big. If something visits the cow and it chases the tiger then the tiger chases the cow.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If something chases the tiger then it visits the cow.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "cow" "+"))
If something chases the cow then the cow is big.
((("something" "chases" "cow" "+")) -> ("cow" "is" "big" "+"))
If something visits the cow and it chases the tiger then the tiger chases the cow.
((("something" "visits" "cow" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
The tiger likes the cow.
True
1
proof
[(triple3)]
("tiger" "likes" "cow" "+")
triple3
The tiger does not like the cow.
False
1
inv-proof
[(triple3)]
("tiger" "likes" "cow" "-")
triple3
The cow visits the cow.
True
2
proof
[(((triple1) -> rule1))]
("cow" "visits" "cow" "+")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "visits" "cow" "-")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The tiger chases the cow.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule3))]
("tiger" "chases" "cow" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The tiger does not chase the cow.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule3))]
("tiger" "chases" "cow" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The tiger does not visit the cow.
Unknown
inv-rconc
[@1: The tiger visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "cow" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cow chases the tiger.[(triple1)] The cow likes the tiger.[(triple2)] The tiger likes the cow.[(triple3)] @1: The cow visits the cow.[(((triple1) -> rule1))] @2: The tiger chases the cow.[(((((triple1) -> rule1) triple1) -> rule3))] @3: The cow is big.[(((((((triple1) -> rule1) triple1) -> rule3)) -> rule2))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple3
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3