The cat is big. The cat likes the lion. The lion chases the cat. The lion is kind. The lion is round. The lion likes the cat. The lion likes the squirrel. The squirrel chases the cat. The squirrel chases the lion. The squirrel eats the cat. The squirrel eats the lion. The squirrel is cold. The squirrel is kind. The squirrel is round. The squirrel likes the cat. The squirrel likes the lion. If someone is cold and rough then they like the squirrel. If someone likes the squirrel and they eat the squirrel then they eat the cat. If someone chases the squirrel and the squirrel is cold then the squirrel is rough. If someone is kind then they chase the squirrel. If someone is cold and they eat the squirrel then the squirrel is round. If the cat is cold and the cat likes the lion then the cat eats the squirrel.
The cat is big.
("cat" "is" "big" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If someone is cold and rough then they like the squirrel.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone likes the squirrel and they eat the squirrel then they eat the cat.
((("someone" "likes" "squirrel" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "eats" "cat" "+"))
If someone chases the squirrel and the squirrel is cold then the squirrel is rough.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "rough" "+"))
If someone is kind then they chase the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is cold and they eat the squirrel then the squirrel is round.
((("someone" "is" "cold" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If the cat is cold and the cat likes the lion then the cat eats the squirrel.
((("cat" "is" "cold" "+") ("cat" "likes" "lion" "+")) -> ("cat" "eats" "squirrel" "+"))
The lion is kind.
True
1
proof
[(triple4)]
("lion" "is" "kind" "+")
triple4
The squirrel is not round.
False
1
inv-proof
[(triple14)]
("squirrel" "is" "round" "-")
triple14
The squirrel chases the squirrel.
True
2
proof
[(((triple13) -> rule4))]
("squirrel" "chases" "squirrel" "+")
((triple13) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The lion does not chase the squirrel.
False
2
inv-proof
[(((triple4) -> rule4))]
("lion" "chases" "squirrel" "-")
((triple4) -> (rule4 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The squirrel is rough.
True
4
proof
[(((((triple13) -> rule4) triple12) -> rule3) OR ((((triple4) -> rule4) triple12) -> rule3))]
("squirrel" "is" "rough" "+")
((((triple13) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
((((triple4) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The squirrel is not rough.
False
4
inv-proof
[(((((triple13) -> rule4) triple12) -> rule3) OR ((((triple4) -> rule4) triple12) -> rule3))]
("squirrel" "is" "rough" "-")
((((triple13) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
((((triple4) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The squirrel likes the squirrel.
True
6
proof
[(((triple12 ((((triple13) -> rule4) triple12) -> rule3)) -> rule1) OR ((triple12 ((((triple4) -> rule4) triple12) -> rule3)) -> rule1))]
("squirrel" "likes" "squirrel" "+")
((triple12 ((((triple13) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((triple12 ((((triple4) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The squirrel does not like the squirrel.
False
6
inv-proof
[(((triple12 ((((triple13) -> rule4) triple12) -> rule3)) -> rule1) OR ((triple12 ((((triple4) -> rule4) triple12) -> rule3)) -> rule1))]
("squirrel" "likes" "squirrel" "-")
((triple12 ((((triple13) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((triple12 ((((triple4) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The cat does not chase the squirrel.
Unknown
inv-rconc
[@1: The cat chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "squirrel" "-")
The cat eats the cat.
Unknown
rconc
[@2: The cat eats the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "eats" "cat" "+")
The cat does not like the squirrel.
Unknown
inv-rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "squirrel" "-")
The lion eats the cat.
Unknown
rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "cat" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat is big.[(triple1)] The cat likes the lion.[(triple2)] The lion chases the cat.[(triple3)] The lion is kind.[(triple4)] The lion is round.[(triple5)] The lion likes the cat.[(triple6)] The lion likes the squirrel.[(triple7)] The squirrel chases the cat.[(triple8)] The squirrel chases the lion.[(triple9)] The squirrel eats the cat.[(triple10)] The squirrel eats the lion.[(triple11)] The squirrel is cold.[(triple12)] The squirrel is kind.[(triple13)] The squirrel is round.[(triple14)] The squirrel likes the cat.[(triple15)] The squirrel likes the lion.[(triple16)] @1: The lion chases the squirrel.[(((triple4) -> rule4))] The squirrel chases the squirrel.[(((triple13) -> rule4))] @2: The squirrel is rough.[(((((triple13) -> rule4) triple12) -> rule3) OR ((((triple4) -> rule4) triple12) -> rule3))] @3: The squirrel likes the squirrel.[(((triple12 ((((triple13) -> rule4) triple12) -> rule3)) -> rule1) OR ((triple12 ((((triple4) -> rule4) triple12) -> rule3)) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The lion chases the cat.
("lion" "chases" "cat" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion likes the cat.
("lion" "likes" "cat" "+")
triple6
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple7
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple8
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple9
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple10
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple11
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple12
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple13
The squirrel is round.
("squirrel" "is" "round" "+")
triple14
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple15
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple16
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple4) -> (rule4 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple13) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple13) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
((((triple4) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple12 ((((triple13) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
((triple12 ((((triple4) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3