The cat is cold. The cat needs the lion. The lion is cold. The lion is rough. The lion needs the cat. The tiger is kind. The tiger sees the lion. If someone needs the tiger then the tiger is young. If the cat chases the lion and the cat needs the tiger then the lion chases the tiger. If someone needs the cat then they chase the tiger. If someone sees the tiger then the tiger sees the lion. If someone is big and they need the cat then the cat is rough. If the lion is kind then the lion sees the tiger. If someone chases the tiger then they are kind. If someone is cold and they need the lion then the lion is rough.
The cat is cold.
("cat" "is" "cold" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone needs the tiger then the tiger is young.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If the cat chases the lion and the cat needs the tiger then the lion chases the tiger.
((("cat" "chases" "lion" "+") ("cat" "needs" "tiger" "+")) -> ("lion" "chases" "tiger" "+"))
If someone needs the cat then they chase the tiger.
((("someone" "needs" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone sees the tiger then the tiger sees the lion.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If someone is big and they need the cat then the cat is rough.
((("someone" "is" "big" "+") ("someone" "needs" "cat" "+")) -> ("cat" "is" "rough" "+"))
If the lion is kind then the lion sees the tiger.
((("lion" "is" "kind" "+")) -> ("lion" "sees" "tiger" "+"))
If someone chases the tiger then they are kind.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and they need the lion then the lion is rough.
((("someone" "is" "cold" "+") ("someone" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
The tiger sees the lion.
True
1
proof
[(triple7 OR ((((((((triple5) -> rule3)) -> rule7)) -> rule6)) -> rule4))]
("tiger" "sees" "lion" "+")
triple7
((((((((triple5) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4
The lion is not cold.
False
1
inv-proof
[(triple3)]
("lion" "is" "cold" "-")
triple3
The lion chases the tiger.
True
2
proof
[(((triple5) -> rule3))]
("lion" "chases" "tiger" "+")
((triple5) -> (rule3 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion does not chase the tiger.
False
2
inv-proof
[(((triple5) -> rule3))]
("lion" "chases" "tiger" "-")
((triple5) -> (rule3 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion is kind.
True
3
proof
[(((((triple5) -> rule3)) -> rule7))]
("lion" "is" "kind" "+")
((((triple5) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion is not kind.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule7))]
("lion" "is" "kind" "-")
((((triple5) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The cat does not chase the tiger.
Unknown
inv-rconc
[@1: The cat chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "tiger" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "young" "+")
The cat is not kind.
Unknown
inv-rconc
[@2: The cat is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("cat" "is" "kind" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not chase the cat.
Unknown
inv-random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat is cold.[(triple1)] The cat needs the lion.[(triple2)] The lion is cold.[(triple3)] The lion is rough.[(triple4 OR ((triple1 triple2) -> rule8))] The lion needs the cat.[(triple5)] The tiger is kind.[(triple6)] The tiger sees the lion.[(triple7 OR ((((((((triple5) -> rule3)) -> rule7)) -> rule6)) -> rule4))] @1: The lion chases the tiger.[(((triple5) -> rule3))] @2: The lion is kind.[(((((triple5) -> rule3)) -> rule7))] @3: The lion sees the tiger.[(((((((triple5) -> rule3)) -> rule7)) -> rule6))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
((triple1 triple2) -> (rule8 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
((((((((triple5) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple5) -> (rule3 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple5) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((((triple5) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3