The dog eats the lion. The lion eats the squirrel. The squirrel does not eat the lion. If the squirrel sees the dog then the dog chases the squirrel. If someone sees the squirrel then they are big. If someone chases the squirrel then they are big. If someone chases the lion and they are nice then the lion is cold. If someone sees the squirrel and they see the lion then the squirrel is cold. If someone sees the squirrel and the squirrel eats the dog then they are cold. If someone eats the lion then the lion sees the squirrel. If the squirrel does not chase the lion then the squirrel eats the lion.
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
If the squirrel sees the dog then the dog chases the squirrel.
((("squirrel" "sees" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If someone sees the squirrel then they are big.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "big" "+"))
If someone chases the squirrel then they are big.
((("someone" "chases" "squirrel" "+")) -> ("someone" "is" "big" "+"))
If someone chases the lion and they are nice then the lion is cold.
((("someone" "chases" "lion" "+") ("someone" "is" "nice" "+")) -> ("lion" "is" "cold" "+"))
If someone sees the squirrel and they see the lion then the squirrel is cold.
((("someone" "sees" "squirrel" "+") ("someone" "sees" "lion" "+")) -> ("squirrel" "is" "cold" "+"))
If someone sees the squirrel and the squirrel eats the dog then they are cold.
((("someone" "sees" "squirrel" "+") ("squirrel" "eats" "dog" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the lion then the lion sees the squirrel.
((("someone" "eats" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If the squirrel does not chase the lion then the squirrel eats the lion.
((("squirrel" "chases" "lion" "~")) -> ("squirrel" "eats" "lion" "+"))
The dog eats the lion.
True
1
proof
[(triple1)]
("dog" "eats" "lion" "+")
triple1
The lion does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "eats" "squirrel" "-")
triple2
The lion sees the squirrel.
True
2
proof
[(((triple1) -> rule7))]
("lion" "sees" "squirrel" "+")
((triple1) -> (rule7 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule7))]
("lion" "sees" "squirrel" "-")
((triple1) -> (rule7 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
True
3
proof
[(((((triple1) -> rule7)) -> rule2))]
("lion" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule2))]
("lion" "is" "big" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "cold" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "cold" "+")
The dog is not big.
Unknown
inv-rconc
[@2: The dog is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("dog" "is" "big" "-")
The dog sees the lion.
Unknown
random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "lion" "+")
The dog does not eat the squirrel.
Unknown
inv-random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "-")
The lion eats the dog.
Unknown
random
[@0: The lion eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "dog" "+")
@0: The dog eats the lion.[(triple1)] The lion eats the squirrel.[(triple2)] The squirrel does not eat the lion.[(triple3)] @1: The lion sees the squirrel.[(((triple1) -> rule7))] @2: The lion is big.[(((((triple1) -> rule7)) -> rule2))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple2
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((triple1) -> (rule7 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2