The cat is not kind. The cow eats the cat. The lion eats the cat. The mouse visits the lion. If someone visits the cow then they see the cat. If someone visits the cow then the cow visits the lion. If someone eats the cat then they visit the cat. If someone eats the cat and they eat the cow then the cow is not blue. If someone visits the lion then they visit the cow. If the cow does not visit the lion and the lion is not nice then the cow visits the cat.
The cat is not kind.
("cat" "is" "kind" "-")
The cow eats the cat.
("cow" "eats" "cat" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone visits the cow then they see the cat.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "cat" "+"))
If someone visits the cow then the cow visits the lion.
((("someone" "visits" "cow" "+")) -> ("cow" "visits" "lion" "+"))
If someone eats the cat then they visit the cat.
((("someone" "eats" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone eats the cat and they eat the cow then the cow is not blue.
((("someone" "eats" "cat" "+") ("someone" "eats" "cow" "+")) -> ("cow" "is" "blue" "-"))
If someone visits the lion then they visit the cow.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "cow" "+"))
If the cow does not visit the lion and the lion is not nice then the cow visits the cat.
((("cow" "visits" "lion" "~") ("lion" "is" "nice" "~")) -> ("cow" "visits" "cat" "+"))
The mouse visits the lion.
True
1
proof
[(triple4)]
("mouse" "visits" "lion" "+")
triple4
The lion does not eat the cat.
False
1
inv-proof
[(triple3)]
("lion" "eats" "cat" "-")
triple3
The mouse visits the cow.
True
2
proof
[(((triple4) -> rule5))]
("mouse" "visits" "cow" "+")
((triple4) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "visits" "cat" "-")
((triple3) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The mouse sees the cat.
True
3
proof
[(((((triple4) -> rule5)) -> rule1))]
("mouse" "sees" "cat" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse does not see the cat.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule1))]
("mouse" "sees" "cat" "-")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cat does not visit the cow.
Unknown
inv-rconc
[@1: The cat visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "cow" "-")
The lion visits the cow.
Unknown
rconc
[@1: The lion visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "cow" "+")
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "cat" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The mouse does not eat the lion.
Unknown
inv-random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cat is not kind.[(triple1)] The cow eats the cat.[(triple2)] The lion eats the cat.[(triple3)] The mouse visits the lion.[(triple4)] @1: The cow visits the cat.[(((triple2) -> rule3))] The lion visits the cat.[(((triple3) -> rule3))] The mouse visits the cow.[(((triple4) -> rule5))] @2: The cow visits the lion.[(((((triple4) -> rule5)) -> rule2))] The mouse sees the cat.[(((((triple4) -> rule5)) -> rule1))] @3: The cow visits the cow.[(((((((triple4) -> rule5)) -> rule2)) -> rule5))] @4: The cow sees the cat.[(((((((((triple4) -> rule5)) -> rule2)) -> rule5)) -> rule1))]
The cat is not kind.
("cat" "is" "kind" "-")
triple1
The cow eats the cat.
("cow" "eats" "cat" "+")
triple2
The lion eats the cat.
("lion" "eats" "cat" "+")
triple3
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple4
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple3) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((triple4) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
int3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int4