The cow is green. The cow is kind. The cow visits the squirrel. The lion is green. The lion is nice. The lion is rough. The lion is young. The lion sees the cow. The lion sees the squirrel. The lion visits the squirrel. The squirrel sees the lion. The squirrel visits the cow. If the lion visits the cow then the cow sees the lion. If someone eats the cow and the cow visits the squirrel then they visit the lion. If someone eats the lion then the lion visits the cow. If the squirrel sees the cow and the squirrel eats the lion then the lion sees the cow. If someone sees the lion and they are rough then they visit the squirrel. If someone visits the cow and the cow visits the squirrel then the cow eats the lion.
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If the lion visits the cow then the cow sees the lion.
((("lion" "visits" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If someone eats the cow and the cow visits the squirrel then they visit the lion.
((("someone" "eats" "cow" "+") ("cow" "visits" "squirrel" "+")) -> ("someone" "visits" "lion" "+"))
If someone eats the lion then the lion visits the cow.
((("someone" "eats" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If the squirrel sees the cow and the squirrel eats the lion then the lion sees the cow.
((("squirrel" "sees" "cow" "+") ("squirrel" "eats" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If someone sees the lion and they are rough then they visit the squirrel.
((("someone" "sees" "lion" "+") ("someone" "is" "rough" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the cow and the cow visits the squirrel then the cow eats the lion.
((("someone" "visits" "cow" "+") ("cow" "visits" "squirrel" "+")) -> ("cow" "eats" "lion" "+"))
The lion visits the squirrel.
True
1
proof
[(triple10)]
("lion" "visits" "squirrel" "+")
triple10
The squirrel does not see the lion.
False
1
inv-proof
[(triple11)]
("squirrel" "sees" "lion" "-")
triple11
The cow eats the lion.
True
3
proof
[(((triple12 triple3) -> rule6))]
("cow" "eats" "lion" "+")
((triple12 triple3) -> (rule6 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow does not eat the lion.
False
3
inv-proof
[(((triple12 triple3) -> rule6))]
("cow" "eats" "lion" "-")
((triple12 triple3) -> (rule6 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The lion visits the cow.
True
4
proof
[(((((triple12 triple3) -> rule6)) -> rule3))]
("lion" "visits" "cow" "+")
((((triple12 triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The lion does not visit the cow.
False
4
inv-proof
[(((((triple12 triple3) -> rule6)) -> rule3))]
("lion" "visits" "cow" "-")
((((triple12 triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow sees the lion.
True
5
proof
[(((((((triple12 triple3) -> rule6)) -> rule3)) -> rule1))]
("cow" "sees" "lion" "+")
((((((triple12 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow does not see the lion.
False
5
inv-proof
[(((((((triple12 triple3) -> rule6)) -> rule3)) -> rule1))]
("cow" "sees" "lion" "-")
((((((triple12 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cow visits the lion.
Unknown
rconc
[@1: The cow visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "lion" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "-")
The squirrel visits the lion.
Unknown
rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "lion" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The cow is green.[(triple1)] The cow is kind.[(triple2)] The cow visits the squirrel.[(triple3)] The lion is green.[(triple4)] The lion is nice.[(triple5)] The lion is rough.[(triple6)] The lion is young.[(triple7)] The lion sees the cow.[(triple8)] The lion sees the squirrel.[(triple9)] The lion visits the squirrel.[(triple10)] The squirrel sees the lion.[(triple11)] The squirrel visits the cow.[(triple12)] @1: The cow eats the lion.[(((triple12 triple3) -> rule6))] @2: The lion visits the cow.[(((((triple12 triple3) -> rule6)) -> rule3))] @3: The cow sees the lion.[(((((((triple12 triple3) -> rule6)) -> rule3)) -> rule1))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is nice.
("lion" "is" "nice" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion is young.
("lion" "is" "young" "+")
triple7
The lion sees the cow.
("lion" "sees" "cow" "+")
triple8
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple9
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple10
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple11
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The cow eats the lion.
("cow" "eats" "lion" "+")
((triple12 triple3) -> (rule6 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
((((triple12 triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow sees the lion.
("cow" "sees" "lion" "+")
((((((triple12 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3