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