The cat is big. The cat is young. The cat needs the tiger. The cat sees the squirrel. The lion needs the cat. The lion visits the tiger. The squirrel is big. The squirrel is rough. The squirrel needs the tiger. The squirrel sees the lion. The tiger visits the cat. The tiger visits the squirrel. If someone is big then they visit the lion. If the tiger needs the squirrel and the squirrel sees the lion then the lion visits the tiger. If someone visits the lion then the lion is big.
The cat is big.
("cat" "is" "big" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone is big then they visit the lion.
((("someone" "is" "big" "+")) -> ("someone" "visits" "lion" "+"))
If the tiger needs the squirrel and the squirrel sees the lion then the lion visits the tiger.
((("tiger" "needs" "squirrel" "+") ("squirrel" "sees" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If someone visits the lion then the lion is big.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "big" "+"))
The squirrel is big.
True
1
proof
[(triple7)]
("squirrel" "is" "big" "+")
triple7
The lion does not need the cat.
False
1
inv-proof
[(triple5)]
("lion" "needs" "cat" "-")
triple5
The squirrel visits the lion.
True
2
proof
[(((triple7) -> rule1))]
("squirrel" "visits" "lion" "+")
((triple7) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The squirrel does not visit the lion.
False
2
inv-proof
[(((triple7) -> rule1))]
("squirrel" "visits" "lion" "-")
((triple7) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The lion is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("lion" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The lion visits the lion.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule1) OR ((((((triple7) -> rule1)) -> rule3)) -> rule1))]
("lion" "visits" "lion" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int3
The lion does not visit the lion.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule1) OR ((((((triple7) -> rule1)) -> rule3)) -> rule1))]
("lion" "visits" "lion" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int3
The tiger does not visit the lion.
Unknown
inv-rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "lion" "-")
The lion needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
The tiger does not need the squirrel.
Unknown
inv-random
[@0: The tiger needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "squirrel" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The lion does not need the squirrel.
Unknown
inv-random
[@0: The lion needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "squirrel" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The cat is big.[(triple1)] The cat is young.[(triple2)] The cat needs the tiger.[(triple3)] The cat sees the squirrel.[(triple4)] The lion needs the cat.[(triple5)] The lion visits the tiger.[(triple6)] The squirrel is big.[(triple7)] The squirrel is rough.[(triple8)] The squirrel needs the tiger.[(triple9)] The squirrel sees the lion.[(triple10)] The tiger visits the cat.[(triple11)] The tiger visits the squirrel.[(triple12)] @1: The cat visits the lion.[(((triple1) -> rule1))] The squirrel visits the lion.[(((triple7) -> rule1))] @2: The lion is big.[(((((triple1) -> rule1)) -> rule3) OR ((((triple7) -> rule1)) -> rule3))] @3: The lion visits the lion.[(((((((triple1) -> rule1)) -> rule3)) -> rule1) OR ((((((triple7) -> rule1)) -> rule3)) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple4
The lion needs the cat.
("lion" "needs" "cat" "+")
triple5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple8
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple11
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple1) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((triple7) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int3