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