The bear visits the cow. The cat does not need the cow. The cow needs the lion. The lion visits the cat. If the lion is young and the lion visits the cat then the cat is not young. If the lion needs the cow then the lion visits the bear. If someone visits the cat and the cat needs the lion then they are not young. If someone visits the cat then they see the cow. If someone needs the lion and the lion does not need the cow then the lion needs the bear. If someone needs the bear then the bear does not need the cow. If someone sees the cow then the cow needs the bear. If the lion sees the bear and the bear is young then the lion sees the cat.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cat does not need the cow.
("cat" "needs" "cow" "-")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If the lion is young and the lion visits the cat then the cat is not young.
((("lion" "is" "young" "+") ("lion" "visits" "cat" "+")) -> ("cat" "is" "young" "-"))
If the lion needs the cow then the lion visits the bear.
((("lion" "needs" "cow" "+")) -> ("lion" "visits" "bear" "+"))
If someone visits the cat and the cat needs the lion then they are not young.
((("someone" "visits" "cat" "+") ("cat" "needs" "lion" "+")) -> ("someone" "is" "young" "-"))
If someone visits the cat then they see the cow.
((("someone" "visits" "cat" "+")) -> ("someone" "sees" "cow" "+"))
If someone needs the lion and the lion does not need the cow then the lion needs the bear.
((("someone" "needs" "lion" "+") ("lion" "needs" "cow" "~")) -> ("lion" "needs" "bear" "+"))
If someone needs the bear then the bear does not need the cow.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "cow" "-"))
If someone sees the cow then the cow needs the bear.
((("someone" "sees" "cow" "+")) -> ("cow" "needs" "bear" "+"))
If the lion sees the bear and the bear is young then the lion sees the cat.
((("lion" "sees" "bear" "+") ("bear" "is" "young" "+")) -> ("lion" "sees" "cat" "+"))
The lion visits the cat.
True
1
proof
[(triple4)]
("lion" "visits" "cat" "+")
triple4
The cow does not need the lion.
False
1
inv-proof
[(triple3)]
("cow" "needs" "lion" "-")
triple3
The lion sees the cow.
True
2
proof
[(((triple4) -> rule4))]
("lion" "sees" "cow" "+")
((triple4) -> (rule4 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion does not see the cow.
False
2
inv-proof
[(((triple4) -> rule4))]
("lion" "sees" "cow" "-")
((triple4) -> (rule4 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow needs the bear.
True
3
proof
[(((((triple4) -> rule4)) -> rule7))]
("cow" "needs" "bear" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow does not need the bear.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule7))]
("cow" "needs" "bear" "-")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The bear does not need the cow.
True
4
proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule6))]
("bear" "needs" "cow" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear does not need the cow.
("bear" "needs" "cow" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The bear needs the cow.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule6))]
("bear" "needs" "cow" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear does not need the cow.
("bear" "needs" "cow" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The cat does not see the cow.
Unknown
inv-rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "cow" "-")
The lion sees the cat.
Unknown
rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "sees" "cat" "+")
The lion does not visit the bear.
Unknown
inv-rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "bear" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "sees" "cow" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
@0: The bear visits the cow.[(triple1)] The cat does not need the cow.[(triple2)] The cow needs the lion.[(triple3)] The lion visits the cat.[(triple4)] @1: The lion sees the cow.[(((triple4) -> rule4))] @2: The cow needs the bear.[(((((triple4) -> rule4)) -> rule7))] @3: The bear does not need the cow.[(((((((triple4) -> rule4)) -> rule7)) -> rule6))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cat does not need the cow.
("cat" "needs" "cow" "-")
triple2
The cow needs the lion.
("cow" "needs" "lion" "+")
triple3
The lion visits the cat.
("lion" "visits" "cat" "+")
triple4
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple4) -> (rule4 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The bear does not need the cow.
("bear" "needs" "cow" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear does not need the cow.
("bear" "needs" "cow" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3