The cat chases the lion. The cat is big. The cat is red. The cat is round. The cat needs the lion. The cat sees the lion. The lion chases the cat. The lion is nice. The lion is red. The lion is round. The lion needs the cat. The lion sees the cat. If something sees the cat then it is not big. If something needs the lion then the lion chases the cat. If something is rough then it chases the cat. If something chases the lion then the lion needs the cat. If the lion sees the cat and the cat does not chase the lion then the cat is red. If something needs the cat then the cat sees the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something sees the cat then it is not big.
((("something" "sees" "cat" "+")) -> ("something" "is" "big" "-"))
If something needs the lion then the lion chases the cat.
((("something" "needs" "lion" "+")) -> ("lion" "chases" "cat" "+"))
If something is rough then it chases the cat.
((("something" "is" "rough" "+")) -> ("something" "chases" "cat" "+"))
If something chases the lion then the lion needs the cat.
((("something" "chases" "lion" "+")) -> ("lion" "needs" "cat" "+"))
If the lion sees the cat and the cat does not chase the lion then the cat is red.
((("lion" "sees" "cat" "+") ("cat" "chases" "lion" "~")) -> ("cat" "is" "red" "+"))
If something needs the cat then the cat sees the lion.
((("something" "needs" "cat" "+")) -> ("cat" "sees" "lion" "+"))
The lion is round.
True
1
proof
[(triple10)]
("lion" "is" "round" "+")
triple10
The cat does not see the lion.
False
1
inv-proof
[(triple6 OR ((triple11) -> rule6) OR ((((triple1) -> rule4)) -> rule6))]
("cat" "sees" "lion" "-")
triple6
((triple11) -> (rule6 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat chases the lion.[(triple1)] The cat is big.[(triple2)] The cat is red.[(triple3)] The cat is round.[(triple4)] The cat needs the lion.[(triple5)] The cat sees the lion.[(triple6 OR ((triple11) -> rule6) OR ((((triple1) -> rule4)) -> rule6))] The lion chases the cat.[(triple7 OR ((triple5) -> rule2))] The lion is nice.[(triple8)] The lion is red.[(triple9)] The lion is round.[(triple10)] The lion needs the cat.[(triple11 OR ((triple1) -> rule4))] The lion sees the cat.[(triple12)] @1: The lion is not big.[(((triple12) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat needs the lion.
("cat" "needs" "lion" "+")
triple5
The cat sees the lion.
("cat" "sees" "lion" "+")
triple6
((triple11) -> (rule6 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
triple7
((triple5) -> (rule2 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion is round.
("lion" "is" "round" "+")
triple10
The lion needs the cat.
("lion" "needs" "cat" "+")
triple11
((triple1) -> (rule4 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
triple12
The lion is not big.
("lion" "is" "big" "-")
((triple12) -> (rule1 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1