The cow visits the lion. The lion does not visit the cow. If something visits the lion then it visits the cow. If something eats the lion then it eats the cow. If something visits the cow then it eats the lion.
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion does not visit the cow.
("lion" "visits" "cow" "-")
If something visits the lion then it visits the cow.
((("something" "visits" "lion" "+")) -> ("something" "visits" "cow" "+"))
If something eats the lion then it eats the cow.
((("something" "eats" "lion" "+")) -> ("something" "eats" "cow" "+"))
If something visits the cow then it eats the lion.
((("something" "visits" "cow" "+")) -> ("something" "eats" "lion" "+"))
The lion does not visit the cow.
True
1
proof
[(triple2)]
("lion" "visits" "cow" "-")
triple2
The cow does not visit the lion.
False
1
inv-proof
[(triple1)]
("cow" "visits" "lion" "-")
triple1
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 cow eats the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("cow" "eats" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow does not eat the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("cow" "eats" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The lion does not eat the cow.
Unknown
inv-rconc
[@2: The lion eats the cow.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("lion" "eats" "cow" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The cow does not like the lion.
Unknown
inv-random
[@0: The cow likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "lion" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The cow visits the lion.[(triple1)] The lion does not visit the cow.[(triple2)] @1: The cow visits the cow.[(((triple1) -> rule1))] @2: The cow eats the lion.[(((((triple1) -> rule1)) -> rule3))] @3: The cow eats the cow.[(((((((triple1) -> rule1)) -> rule3)) -> rule2))]
The cow visits the lion.
("cow" "visits" "lion" "+")
triple1
The lion does not visit the cow.
("lion" "visits" "cow" "-")
triple2
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3