The dog chases the lion. The dog eats the rabbit. The dog is not cold. The lion is not cold. The lion is red. The lion sees the rabbit. The rabbit does not chase the dog. The rabbit eats the dog. The rabbit eats the lion. The rabbit eats the squirrel. The rabbit is big. The squirrel sees the rabbit. If someone chases the rabbit and the rabbit eats the lion then they do not chase the dog. If someone eats the lion and they are not cold then the lion is red. If someone chases the squirrel then they chase the rabbit. Round people are big. If someone chases the lion then they are not big. If someone is blue then they are not red. If someone is cold and round then they do not eat the squirrel. If someone chases the lion and the lion is big then the lion chases the squirrel. If someone is red then they are round.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is not cold.
("dog" "is" "cold" "-")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is red.
("lion" "is" "red" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit does not chase the dog.
("rabbit" "chases" "dog" "-")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone chases the rabbit and the rabbit eats the lion then they do not chase the dog.
((("someone" "chases" "rabbit" "+") ("rabbit" "eats" "lion" "+")) -> ("someone" "chases" "dog" "-"))
If someone eats the lion and they are not cold then the lion is red.
((("someone" "eats" "lion" "+") ("someone" "is" "cold" "~")) -> ("lion" "is" "red" "+"))
If someone chases the squirrel then they chase the rabbit.
((("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "rabbit" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone chases the lion then they are not big.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "big" "-"))
If someone is blue then they are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
If someone is cold and round then they do not eat the squirrel.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "eats" "squirrel" "-"))
If someone chases the lion and the lion is big then the lion chases the squirrel.
((("someone" "chases" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "chases" "squirrel" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
The rabbit eats the dog.
True
1
proof
[(triple8)]
("rabbit" "eats" "dog" "+")
triple8
The lion is not red.
False
1
inv-proof
[(triple5)]
("lion" "is" "red" "-")
triple5
The lion is round.
True
2
proof
[(((triple5) -> rule9))]
("lion" "is" "round" "+")
((triple5) -> (rule9 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple5) -> rule9))]
("lion" "is" "round" "-")
((triple5) -> (rule9 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is big.
True
3
proof
[(((((triple5) -> rule9)) -> rule4))]
("lion" "is" "big" "+")
((((triple5) -> (rule9 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple5) -> rule9)) -> rule4))]
("lion" "is" "big" "-")
((((triple5) -> (rule9 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion chases the squirrel.
True
5
proof
[(((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8))]
("lion" "chases" "squirrel" "+")
((triple1 ((((triple5) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion does not chase the squirrel.
False
5
inv-proof
[(((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8))]
("lion" "chases" "squirrel" "-")
((triple1 ((((triple5) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion chases the rabbit.
True
6
proof
[(((((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8)) -> rule3))]
("lion" "chases" "rabbit" "+")
((((triple1 ((((triple5) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is round.
("lion" "is" "round" "+")
int4
The lion does not chase the rabbit.
False
6
inv-proof
[(((((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8)) -> rule3))]
("lion" "chases" "rabbit" "-")
((((triple1 ((((triple5) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is round.
("lion" "is" "round" "+")
int4
The lion does not chase the dog.
True
8
proof
[(((((((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8)) -> rule3) triple9) -> rule1))]
("lion" "chases" "dog" "-")
((((((triple1 ((((triple5) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
The lion does not chase the dog.
("lion" "chases" "dog" "-")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion is round.
("lion" "is" "round" "+")
int5
The lion chases the dog.
False
8
inv-proof
[(((((((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8)) -> rule3) triple9) -> rule1))]
("lion" "chases" "dog" "+")
((((((triple1 ((((triple5) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
The lion does not chase the dog.
("lion" "chases" "dog" "-")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion is round.
("lion" "is" "round" "+")
int5
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("dog" "is" "round" "-")
The squirrel is big.
Unknown
rconc
[@2: The squirrel is big.[CWA. Example of deepest failure = (rule4 <- rule9 <- FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not chase the rabbit.
Unknown
inv-rconc
[@1: The squirrel chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "rabbit" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("rabbit" "is" "round" "+")
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The squirrel does not chase the lion.
Unknown
inv-random
[@0: The squirrel chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "lion" "-")
The rabbit sees the squirrel.
Unknown
random
[@0: The rabbit sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "squirrel" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit chases the lion.
Unknown
random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "+")
@0: The dog chases the lion.[(triple1)] The dog eats the rabbit.[(triple2)] The dog is not cold.[(triple3)] The lion is not cold.[(triple4)] The lion is red.[(triple5)] The lion sees the rabbit.[(triple6)] The rabbit does not chase the dog.[(triple7)] The rabbit eats the dog.[(triple8)] The rabbit eats the lion.[(triple9)] The rabbit eats the squirrel.[(triple10)] The rabbit is big.[(triple11)] The squirrel sees the rabbit.[(triple12)] @1: The dog is not big.[(((triple1) -> rule5))] The lion is round.[(((triple5) -> rule9))] @2: The lion is big.[(((((triple5) -> rule9)) -> rule4))] @3: The lion chases the squirrel.[(((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8))] @4: The lion chases the rabbit.[(((((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8)) -> rule3))] @5: The lion does not chase the dog.[(((((((triple1 ((((triple5) -> rule9)) -> rule4)) -> rule8)) -> rule3) triple9) -> rule1))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
The dog is not cold.
("dog" "is" "cold" "-")
triple3
The lion is not cold.
("lion" "is" "cold" "-")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple6
The rabbit does not chase the dog.
("rabbit" "chases" "dog" "-")
triple7
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple8
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple9
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple12
The dog is not big.
("dog" "is" "big" "-")
((triple1) -> (rule5 % int1))
The dog is not big.
("dog" "is" "big" "-")
int1
The lion is round.
("lion" "is" "round" "+")
((triple5) -> (rule9 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple5) -> (rule9 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple1 ((((triple5) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((((triple1 ((((triple5) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is round.
("lion" "is" "round" "+")
int4
The lion does not chase the dog.
("lion" "chases" "dog" "-")
((((((triple1 ((((triple5) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
The lion does not chase the dog.
("lion" "chases" "dog" "-")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion is round.
("lion" "is" "round" "+")
int5