The cow likes the tiger. The tiger visits the cow. If something visits the tiger and it eats the tiger then it eats the cow. If something visits the cow and the cow visits the tiger then it eats the tiger. If something eats the cow and the cow likes the tiger then the cow visits the tiger. If something likes the tiger and the tiger visits the cow then the tiger eats the cow. If something likes the tiger and the tiger is red then it likes the cow. If something eats the cow then it visits the cow.
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something visits the tiger and it eats the tiger then it eats the cow.
((("something" "visits" "tiger" "+") ("something" "eats" "tiger" "+")) -> ("something" "eats" "cow" "+"))
If something visits the cow and the cow visits the tiger then it eats the tiger.
((("something" "visits" "cow" "+") ("cow" "visits" "tiger" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the cow and the cow likes the tiger then the cow visits the tiger.
((("something" "eats" "cow" "+") ("cow" "likes" "tiger" "+")) -> ("cow" "visits" "tiger" "+"))
If something likes the tiger and the tiger visits the cow then the tiger eats the cow.
((("something" "likes" "tiger" "+") ("tiger" "visits" "cow" "+")) -> ("tiger" "eats" "cow" "+"))
If something likes the tiger and the tiger is red then it likes the cow.
((("something" "likes" "tiger" "+") ("tiger" "is" "red" "+")) -> ("something" "likes" "cow" "+"))
If something eats the cow then it visits the cow.
((("something" "eats" "cow" "+")) -> ("something" "visits" "cow" "+"))
The cow likes the tiger.
True
1
proof
[(triple1)]
("cow" "likes" "tiger" "+")
triple1
The cow does not like the tiger.
False
1
inv-proof
[(triple1)]
("cow" "likes" "tiger" "-")
triple1
The tiger eats the cow.
True
3
proof
[(((triple1 triple2) -> rule4))]
("tiger" "eats" "cow" "+")
((triple1 triple2) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger does not eat the cow.
False
3
inv-proof
[(((triple1 triple2) -> rule4))]
("tiger" "eats" "cow" "-")
((triple1 triple2) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The cow visits the tiger.
True
5
proof
[(((((triple1 triple2) -> rule4) triple1) -> rule3))]
("cow" "visits" "tiger" "+")
((((triple1 triple2) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The cow does not visit the tiger.
False
5
inv-proof
[(((((triple1 triple2) -> rule4) triple1) -> rule3))]
("cow" "visits" "tiger" "-")
((((triple1 triple2) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The tiger eats the tiger.
True
7
proof
[(((triple2 ((((triple1 triple2) -> rule4) triple1) -> rule3)) -> rule2))]
("tiger" "eats" "tiger" "+")
((triple2 ((((triple1 triple2) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int3
The tiger does not eat the tiger.
False
7
inv-proof
[(((triple2 ((((triple1 triple2) -> rule4) triple1) -> rule3)) -> rule2))]
("tiger" "eats" "tiger" "-")
((triple2 ((((triple1 triple2) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int3
The tiger does not like the cow.
Unknown
inv-rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "cow" "-")
The cow eats the tiger.
Unknown
rconc
[@3: The cow eats the tiger.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule1 <- FAIL)]]
("cow" "eats" "tiger" "+")
The cow does not eat the cow.
Unknown
inv-rconc
[@3: The cow eats the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule6 <- FAIL)]]
("cow" "eats" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@3: The cow visits the cow.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule2 <- FAIL)]]
("cow" "visits" "cow" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cow likes the tiger.[(triple1)] The tiger visits the cow.[(triple2)] @1: The tiger eats the cow.[(((triple1 triple2) -> rule4))] @2: The cow visits the tiger.[(((((triple1 triple2) -> rule4) triple1) -> rule3))] @3: The tiger eats the tiger.[(((triple2 ((((triple1 triple2) -> rule4) triple1) -> rule3)) -> rule2))]
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
((triple1 triple2) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((((triple1 triple2) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple2 ((((triple1 triple2) -> (rule4 % int3)) triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int3