The cat is round. The cat visits the squirrel. The lion chases the squirrel. The lion is big. The squirrel chases the cat. The squirrel eats the lion. The squirrel is rough. All rough things are big. If something visits the cat and it chases the squirrel then the cat chases the lion. If something is round and it chases the squirrel then the squirrel eats the lion. Nice things are big. If something is big and it chases the cat then the cat is rough. If something chases the lion then the lion is green. If something chases the squirrel and the squirrel visits the lion then it is round. If something is round then it eats the squirrel.
The cat is round.
("cat" "is" "round" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something visits the cat and it chases the squirrel then the cat chases the lion.
((("something" "visits" "cat" "+") ("something" "chases" "squirrel" "+")) -> ("cat" "chases" "lion" "+"))
If something is round and it chases the squirrel then the squirrel eats the lion.
((("something" "is" "round" "+") ("something" "chases" "squirrel" "+")) -> ("squirrel" "eats" "lion" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is big and it chases the cat then the cat is rough.
((("something" "is" "big" "+") ("something" "chases" "cat" "+")) -> ("cat" "is" "rough" "+"))
If something chases the lion then the lion is green.
((("something" "chases" "lion" "+")) -> ("lion" "is" "green" "+"))
If something chases the squirrel and the squirrel visits the lion then it is round.
((("something" "chases" "squirrel" "+") ("squirrel" "visits" "lion" "+")) -> ("something" "is" "round" "+"))
If something is round then it eats the squirrel.
((("something" "is" "round" "+")) -> ("something" "eats" "squirrel" "+"))
The squirrel eats the lion.
True
1
proof
[(triple6)]
("squirrel" "eats" "lion" "+")
triple6
The lion is not big.
False
1
inv-proof
[(triple4)]
("lion" "is" "big" "-")
triple4
The squirrel is big.
True
2
proof
[(((triple7) -> rule1))]
("squirrel" "is" "big" "+")
((triple7) -> (rule1 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "eats" "squirrel" "-")
((triple1) -> (rule8 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is rough.
True
4
proof
[(((((triple7) -> rule1) triple5) -> rule5))]
("cat" "is" "rough" "+")
((((triple7) -> (rule1 % int2)) triple5) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat is not rough.
False
4
inv-proof
[(((((triple7) -> rule1) triple5) -> rule5))]
("cat" "is" "rough" "-")
((((triple7) -> (rule1 % int2)) triple5) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat is big.
True
5
proof
[(((((((triple7) -> rule1) triple5) -> rule5)) -> rule1))]
("cat" "is" "big" "+")
((((((triple7) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The cat is not big.
False
5
inv-proof
[(((((((triple7) -> rule1) triple5) -> rule5)) -> rule1))]
("cat" "is" "big" "-")
((((((triple7) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@2: The lion is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "is" "green" "-")
The cat chases the lion.
Unknown
rconc
[@1: The cat chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "lion" "+")
The lion does not eat the squirrel.
Unknown
inv-rconc
[@2: The lion eats the squirrel.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("lion" "eats" "squirrel" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "round" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not chase the cat.
Unknown
inv-random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is round.[(triple1)] The cat visits the squirrel.[(triple2)] The lion chases the squirrel.[(triple3)] The lion is big.[(triple4)] The squirrel chases the cat.[(triple5)] The squirrel eats the lion.[(triple6)] The squirrel is rough.[(triple7)] @1: The cat eats the squirrel.[(((triple1) -> rule8))] The squirrel is big.[(((triple7) -> rule1))] @2: The cat is rough.[(((((triple7) -> rule1) triple5) -> rule5))] @3: The cat is big.[(((((((triple7) -> rule1) triple5) -> rule5)) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
triple4
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple5
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple6
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple7
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((triple1) -> (rule8 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple7) -> (rule1 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple7) -> (rule1 % int2)) triple5) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat is big.
("cat" "is" "big" "+")
((((((triple7) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3