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