The cat chases the lion. The cat eats the lion. The cat is big. The cat is green. The cat is nice. The cat is rough. The cat is young. The cat sees the lion. The lion chases the cat. The lion eats the cat. The lion is green. The lion is nice. The lion is rough. The lion is young. The lion sees the cat. If something is young then it eats the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something is young then it eats the lion.
((("something" "is" "young" "+")) -> ("something" "eats" "lion" "+"))
The cat is rough.
True
1
proof
[(triple6)]
("cat" "is" "rough" "+")
triple6
The lion does not chase the cat.
False
1
inv-proof
[(triple9)]
("lion" "chases" "cat" "-")
triple9
The lion eats the lion.
True
2
proof
[(((triple14) -> rule1))]
("lion" "eats" "lion" "+")
((triple14) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not eat the lion.
False
2
inv-proof
[(((triple14) -> rule1))]
("lion" "eats" "lion" "-")
((triple14) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat chases the lion.[(triple1)] The cat eats the lion.[(triple2 OR ((triple7) -> rule1))] The cat is big.[(triple3)] The cat is green.[(triple4)] The cat is nice.[(triple5)] The cat is rough.[(triple6)] The cat is young.[(triple7)] The cat sees the lion.[(triple8)] The lion chases the cat.[(triple9)] The lion eats the cat.[(triple10)] The lion is green.[(triple11)] The lion is nice.[(triple12)] The lion is rough.[(triple13)] The lion is young.[(triple14)] The lion sees the cat.[(triple15)] @1: The lion eats the lion.[(((triple14) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
((triple7) -> (rule1 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat is young.
("cat" "is" "young" "+")
triple7
The cat sees the lion.
("cat" "sees" "lion" "+")
triple8
The lion chases the cat.
("lion" "chases" "cat" "+")
triple9
The lion eats the cat.
("lion" "eats" "cat" "+")
triple10
The lion is green.
("lion" "is" "green" "+")
triple11
The lion is nice.
("lion" "is" "nice" "+")
triple12
The lion is rough.
("lion" "is" "rough" "+")
triple13
The lion is young.
("lion" "is" "young" "+")
triple14
The lion sees the cat.
("lion" "sees" "cat" "+")
triple15
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple14) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1