The lion chases the tiger. The lion is big. The lion is green. The lion is nice. The lion sees the rabbit. The lion sees the tiger. The lion visits the tiger. The rabbit chases the lion. The rabbit chases the tiger. The rabbit is kind. The rabbit is red. The rabbit visits the tiger. The tiger chases the lion. The tiger is big. The tiger is red. The tiger visits the rabbit. If something is big and it sees the tiger then it sees the rabbit. If something sees the rabbit and it chases the lion then the rabbit chases the tiger. If the tiger is big then the tiger chases the rabbit. If something is red and it chases the tiger then it visits the rabbit. If something sees the rabbit then the rabbit visits the lion. If something is big then it visits the lion. If something sees the rabbit then it chases the rabbit. If something visits the lion then it chases the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something is big and it sees the tiger then it sees the rabbit.
((("something" "is" "big" "+") ("something" "sees" "tiger" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the rabbit and it chases the lion then the rabbit chases the tiger.
((("something" "sees" "rabbit" "+") ("something" "chases" "lion" "+")) -> ("rabbit" "chases" "tiger" "+"))
If the tiger is big then the tiger chases the rabbit.
((("tiger" "is" "big" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something is red and it chases the tiger then it visits the rabbit.
((("something" "is" "red" "+") ("something" "chases" "tiger" "+")) -> ("something" "visits" "rabbit" "+"))
If something sees the rabbit then the rabbit visits the lion.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
If something is big then it visits the lion.
((("something" "is" "big" "+")) -> ("something" "visits" "lion" "+"))
If something sees the rabbit then it chases the rabbit.
((("something" "sees" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
If something visits the lion then it chases the lion.
((("something" "visits" "lion" "+")) -> ("something" "chases" "lion" "+"))
The lion is green.
True
1
proof
[(triple3)]
("lion" "is" "green" "+")
triple3
The tiger does not visit the rabbit.
False
1
inv-proof
[(triple16)]
("tiger" "visits" "rabbit" "-")
triple16
The lion visits the lion.
True
2
proof
[(((triple2) -> rule6))]
("lion" "visits" "lion" "+")
((triple2) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The tiger does not visit the lion.
False
2
inv-proof
[(((triple14) -> rule6))]
("tiger" "visits" "lion" "-")
((triple14) -> (rule6 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion chases the lion.
True
3
proof
[(((((triple2) -> rule6)) -> rule8))]
("lion" "chases" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion does not chase the lion.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule8))]
("lion" "chases" "lion" "-")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The tiger does not see the rabbit.
Unknown
inv-rconc
[@1: The tiger sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "rabbit" "-")
The lion visits the rabbit.
Unknown
rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit sees the lion.
Unknown
random
[@0: The rabbit sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "lion" "+")
@0: The lion chases the tiger.[(triple1)] The lion is big.[(triple2)] The lion is green.[(triple3)] The lion is nice.[(triple4)] The lion sees the rabbit.[(triple5 OR ((triple2 triple6) -> rule1))] The lion sees the tiger.[(triple6)] The lion visits the tiger.[(triple7)] The rabbit chases the lion.[(triple8 OR ((((triple5) -> rule5)) -> rule8) OR ((((((triple2 triple6) -> rule1)) -> rule5)) -> rule8))] The rabbit chases the tiger.[(triple9 OR ((triple5 ((((triple2) -> rule6)) -> rule8)) -> rule2) OR ((((triple2 triple6) -> rule1) ((((triple2) -> rule6)) -> rule8)) -> rule2))] The rabbit is kind.[(triple10)] The rabbit is red.[(triple11)] The rabbit visits the tiger.[(triple12)] The tiger chases the lion.[(triple13 OR ((((triple14) -> rule6)) -> rule8))] The tiger is big.[(triple14)] The tiger is red.[(triple15)] The tiger visits the rabbit.[(triple16)] @1: The lion chases the rabbit.[(((triple5) -> rule7) OR ((((triple2 triple6) -> rule1)) -> rule7))] The lion visits the lion.[(((triple2) -> rule6))] The rabbit visits the lion.[(((triple5) -> rule5) OR ((((triple2 triple6) -> rule1)) -> rule5))] The rabbit visits the rabbit.[(((triple11 triple9) -> rule4) OR ((triple11 ((triple5 ((((triple2) -> rule6)) -> rule8)) -> rule2)) -> rule4) OR ((triple11 ((((triple2 triple6) -> rule1) ((((triple2) -> rule6)) -> rule8)) -> rule2)) -> rule4))] The tiger chases the rabbit.[(((triple14) -> rule3))] The tiger visits the lion.[(((triple14) -> rule6))] @2: The lion chases the lion.[(((((triple2) -> rule6)) -> rule8))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple5
((triple2 triple6) -> (rule1 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple6
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple7
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple8
((((triple5) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int2
((((((triple2 triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int3
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple9
((triple5 ((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
((((triple2 triple6) -> (rule1 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple12
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple13
((((triple14) -> (rule6 % int2))) -> (rule8 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
triple14
The tiger is red.
("tiger" "is" "red" "+")
triple15
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple16
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple5) -> (rule7 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
((((triple2 triple6) -> (rule1 % int2))) -> (rule7 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple2) -> (rule6 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((triple5) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
((((triple2 triple6) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple11 triple9) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
((triple11 ((triple5 ((((triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
((triple11 ((((triple2 triple6) -> (rule1 % int5)) ((((triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int5
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple14) -> (rule3 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple14) -> (rule6 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2