The bear is rough. The bear is round. The cat chases the rabbit. The cat chases the tiger. The rabbit is round. The rabbit needs the tiger. The tiger needs the bear. If the rabbit visits the cat then the rabbit visits the tiger. If something chases the rabbit then the rabbit chases the cat. If something needs the bear and the bear is round then it chases the cat. If the bear visits the cat and the bear needs the cat then the bear needs the tiger. If something chases the rabbit and it chases the tiger then the tiger needs the bear. If something visits the rabbit and the rabbit is rough then the rabbit is green. If something visits the tiger and it needs the tiger then the tiger is round. If something needs the tiger then it visits the cat.
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If the rabbit visits the cat then the rabbit visits the tiger.
((("rabbit" "visits" "cat" "+")) -> ("rabbit" "visits" "tiger" "+"))
If something chases the rabbit then the rabbit chases the cat.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cat" "+"))
If something needs the bear and the bear is round then it chases the cat.
((("something" "needs" "bear" "+") ("bear" "is" "round" "+")) -> ("something" "chases" "cat" "+"))
If the bear visits the cat and the bear needs the cat then the bear needs the tiger.
((("bear" "visits" "cat" "+") ("bear" "needs" "cat" "+")) -> ("bear" "needs" "tiger" "+"))
If something chases the rabbit and it chases the tiger then the tiger needs the bear.
((("something" "chases" "rabbit" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "needs" "bear" "+"))
If something visits the rabbit and the rabbit is rough then the rabbit is green.
((("something" "visits" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "green" "+"))
If something visits the tiger and it needs the tiger then the tiger is round.
((("something" "visits" "tiger" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If something needs the tiger then it visits the cat.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "cat" "+"))
The bear is round.
True
1
proof
[(triple2)]
("bear" "is" "round" "+")
triple2
The rabbit does not need the tiger.
False
1
inv-proof
[(triple6)]
("rabbit" "needs" "tiger" "-")
triple6
The tiger chases the cat.
True
3
proof
[(((triple7 triple2) -> rule3) OR ((((triple3 triple4) -> rule5) triple2) -> rule3))]
("tiger" "chases" "cat" "+")
((triple7 triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((((triple3 triple4) -> (rule5 % int2)) triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger does not chase the cat.
False
3
inv-proof
[(((triple7 triple2) -> rule3) OR ((((triple3 triple4) -> rule5) triple2) -> rule3))]
("tiger" "chases" "cat" "-")
((triple7 triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((((triple3 triple4) -> (rule5 % int2)) triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The rabbit visits the tiger.
True
3
proof
[(((((triple6) -> rule8)) -> rule1))]
("rabbit" "visits" "tiger" "+")
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit does not visit the tiger.
False
3
inv-proof
[(((((triple6) -> rule8)) -> rule1))]
("rabbit" "visits" "tiger" "-")
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The tiger is round.
True
5
proof
[(((((((triple6) -> rule8)) -> rule1) triple6) -> rule7))]
("tiger" "is" "round" "+")
((((((triple6) -> (rule8 % int3))) -> (rule1 % int2)) triple6) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3
The tiger is not round.
False
5
inv-proof
[(((((((triple6) -> rule8)) -> rule1) triple6) -> rule7))]
("tiger" "is" "round" "-")
((((((triple6) -> (rule8 % int3))) -> (rule1 % int2)) triple6) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "visits" "cat" "-")
The bear needs the tiger.
Unknown
rconc
[@1: The bear needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "needs" "tiger" "+")
The bear does not visit the cat.
Unknown
inv-rconc
[@2: The bear visits the cat.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("bear" "visits" "cat" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "green" "+")
The cat does not visit the tiger.
Unknown
inv-random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The bear is rough.[(triple1)] The bear is round.[(triple2)] The cat chases the rabbit.[(triple3)] The cat chases the tiger.[(triple4)] The rabbit is round.[(triple5)] The rabbit needs the tiger.[(triple6)] The tiger needs the bear.[(triple7 OR ((triple3 triple4) -> rule5))] @1: The rabbit chases the cat.[(((triple3) -> rule2))] The rabbit visits the cat.[(((triple6) -> rule8))] The tiger chases the cat.[(((triple7 triple2) -> rule3) OR ((((triple3 triple4) -> rule5) triple2) -> rule3))] @2: The rabbit visits the tiger.[(((((triple6) -> rule8)) -> rule1))] @3: The tiger is round.[(((((((triple6) -> rule8)) -> rule1) triple6) -> rule7))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple3
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple6
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple7
((triple3 triple4) -> (rule5 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
((triple3) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple6) -> (rule8 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple7 triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((((triple3 triple4) -> (rule5 % int2)) triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((((triple6) -> (rule8 % int3))) -> (rule1 % int2)) triple6) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3