The cat chases the tiger. The cat is cold. The cat is not nice. The cat is not rough. The lion is not red. The rabbit sees the tiger. The tiger sees the lion. If something is cold then it visits the lion. If the tiger sees the rabbit then the rabbit chases the lion. If the cat visits the lion then the lion is cold. If something sees the tiger and the tiger is cold then the tiger visits the lion. If the cat does not visit the rabbit then the rabbit is not cold. If the lion chases the rabbit and the rabbit is not nice then the lion does not see the rabbit.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is not rough.
("cat" "is" "rough" "-")
The lion is not red.
("lion" "is" "red" "-")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something is cold then it visits the lion.
((("something" "is" "cold" "+")) -> ("something" "visits" "lion" "+"))
If the tiger sees the rabbit then the rabbit chases the lion.
((("tiger" "sees" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
If the cat visits the lion then the lion is cold.
((("cat" "visits" "lion" "+")) -> ("lion" "is" "cold" "+"))
If something sees the tiger and the tiger is cold then the tiger visits the lion.
((("something" "sees" "tiger" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "visits" "lion" "+"))
If the cat does not visit the rabbit then the rabbit is not cold.
((("cat" "visits" "rabbit" "~")) -> ("rabbit" "is" "cold" "-"))
If the lion chases the rabbit and the rabbit is not nice then the lion does not see the rabbit.
((("lion" "chases" "rabbit" "+") ("rabbit" "is" "nice" "~")) -> ("lion" "sees" "rabbit" "-"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The cat is nice.
False
1
inv-proof
[(triple3)]
("cat" "is" "nice" "+")
triple3
The cat visits the lion.
True
2
proof
[(((triple2) -> rule1))]
("cat" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat does not visit the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "visits" "lion" "-")
((triple2) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion is cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("lion" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion is not cold.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("lion" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion visits the lion.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule1))]
("lion" "visits" "lion" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The lion does not visit the lion.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule1))]
("lion" "visits" "lion" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The rabbit does not visit the lion.
Unknown
inv-rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "lion" "-")
The rabbit chases the lion.
Unknown
rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "lion" "+")
The tiger does not visit the lion.
Unknown
inv-rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "lion" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat sees the lion.
Unknown
random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "+")
@0: The cat chases the tiger.[(triple1)] The cat is cold.[(triple2)] The cat is not nice.[(triple3)] The cat is not rough.[(triple4)] The lion is not red.[(triple5)] The rabbit sees the tiger.[(triple6)] The tiger sees the lion.[(triple7)] @1: The cat visits the lion.[(((triple2) -> rule1))] @2: The lion is cold.[(((((triple2) -> rule1)) -> rule3))] @3: The lion visits the lion.[(((((((triple2) -> rule1)) -> rule3)) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is not nice.
("cat" "is" "nice" "-")
triple3
The cat is not rough.
("cat" "is" "rough" "-")
triple4
The lion is not red.
("lion" "is" "red" "-")
triple5
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3