The cow is nice. The cow does not visit the tiger. The lion does not visit the tiger. The rabbit visits the tiger. The tiger eats the cow. The tiger eats the rabbit. The tiger sees the lion. If the tiger eats the cow and the cow visits the lion then the tiger visits the cow. If someone sees the tiger and the tiger visits the lion then the tiger eats the cow. If someone is nice then they visit the lion. If someone visits the cow and the cow eats the rabbit then the cow eats the tiger. If someone eats the lion and they do not visit the cow then the cow eats the rabbit. If someone sees the rabbit and they do not eat the cow then the cow is not round.
The cow is nice.
("cow" "is" "nice" "+")
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the tiger eats the cow and the cow visits the lion then the tiger visits the cow.
((("tiger" "eats" "cow" "+") ("cow" "visits" "lion" "+")) -> ("tiger" "visits" "cow" "+"))
If someone sees the tiger and the tiger visits the lion then the tiger eats the cow.
((("someone" "sees" "tiger" "+") ("tiger" "visits" "lion" "+")) -> ("tiger" "eats" "cow" "+"))
If someone is nice then they visit the lion.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the cow and the cow eats the rabbit then the cow eats the tiger.
((("someone" "visits" "cow" "+") ("cow" "eats" "rabbit" "+")) -> ("cow" "eats" "tiger" "+"))
If someone eats the lion and they do not visit the cow then the cow eats the rabbit.
((("someone" "eats" "lion" "+") ("someone" "visits" "cow" "~")) -> ("cow" "eats" "rabbit" "+"))
If someone sees the rabbit and they do not eat the cow then the cow is not round.
((("someone" "sees" "rabbit" "+") ("someone" "eats" "cow" "~")) -> ("cow" "is" "round" "-"))
The lion does not visit the tiger.
True
1
proof
[(triple3)]
("lion" "visits" "tiger" "-")
triple3
The rabbit does not visit the tiger.
False
1
inv-proof
[(triple4)]
("rabbit" "visits" "tiger" "-")
triple4
The cow visits the lion.
True
2
proof
[(((triple1) -> rule3))]
("cow" "visits" "lion" "+")
((triple1) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "visits" "lion" "-")
((triple1) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The tiger visits the cow.
True
4
proof
[(((triple5 ((triple1) -> rule3)) -> rule1))]
("tiger" "visits" "cow" "+")
((triple5 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The tiger does not visit the cow.
False
4
inv-proof
[(((triple5 ((triple1) -> rule3)) -> rule1))]
("tiger" "visits" "cow" "-")
((triple5 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The tiger does not visit the lion.
Unknown
inv-rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "lion" "-")
The rabbit visits the lion.
Unknown
rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "lion" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The cow does not see the lion.
Unknown
inv-random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
@0: The cow does not visit the tiger.[(triple2)] The cow is nice.[(triple1)] The lion does not visit the tiger.[(triple3)] The rabbit visits the tiger.[(triple4)] The tiger eats the cow.[(triple5)] The tiger eats the rabbit.[(triple6)] The tiger sees the lion.[(triple7)] @1: The cow visits the lion.[(((triple1) -> rule3))] @2: The tiger visits the cow.[(((triple5 ((triple1) -> rule3)) -> rule1))]
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple1
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
triple3
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple4
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple5
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple1) -> (rule3 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple5 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2