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