The cat is rough. The cat likes the rabbit. The lion is rough. The lion likes the mouse. The mouse is rough. The mouse likes the cat. The mouse likes the rabbit. The mouse visits the cat. The mouse does not visit the rabbit. The rabbit is rough. The rabbit visits the cat. If someone visits the cat then they chase the cat. If someone visits the cat and they like the mouse then the cat chases the rabbit. If the lion visits the cat then the lion is cold. If someone visits the lion then they are not rough. If someone is big and they like the lion then they visit the mouse. If someone chases the rabbit then they like the mouse. If someone chases the cat then they chase the rabbit.
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone visits the cat then they chase the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If someone visits the cat and they like the mouse then the cat chases the rabbit.
((("someone" "visits" "cat" "+") ("someone" "likes" "mouse" "+")) -> ("cat" "chases" "rabbit" "+"))
If the lion visits the cat then the lion is cold.
((("lion" "visits" "cat" "+")) -> ("lion" "is" "cold" "+"))
If someone visits the lion then they are not rough.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "rough" "-"))
If someone is big and they like the lion then they visit the mouse.
((("someone" "is" "big" "+") ("someone" "likes" "lion" "+")) -> ("someone" "visits" "mouse" "+"))
If someone chases the rabbit then they like the mouse.
((("someone" "chases" "rabbit" "+")) -> ("someone" "likes" "mouse" "+"))
If someone chases the cat then they chase the rabbit.
((("someone" "chases" "cat" "+")) -> ("someone" "chases" "rabbit" "+"))
The rabbit visits the cat.
True
1
proof
[(triple11)]
("rabbit" "visits" "cat" "+")
triple11
The mouse does not like the rabbit.
False
1
inv-proof
[(triple7)]
("mouse" "likes" "rabbit" "-")
triple7
The rabbit chases the cat.
True
2
proof
[(((triple11) -> rule1))]
("rabbit" "chases" "cat" "+")
((triple11) -> (rule1 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The mouse does not chase the cat.
False
2
inv-proof
[(((triple8) -> rule1))]
("mouse" "chases" "cat" "-")
((triple8) -> (rule1 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse chases the rabbit.
True
3
proof
[(((((triple8) -> rule1)) -> rule7))]
("mouse" "chases" "rabbit" "+")
((((triple8) -> (rule1 % int2))) -> (rule7 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((((triple11) -> rule1)) -> rule7))]
("rabbit" "chases" "rabbit" "-")
((((triple11) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit likes the mouse.
True
4
proof
[(((((((triple11) -> rule1)) -> rule7)) -> rule6))]
("rabbit" "likes" "mouse" "+")
((((((triple11) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The rabbit does not like the mouse.
False
4
inv-proof
[(((((((triple11) -> rule1)) -> rule7)) -> rule6))]
("rabbit" "likes" "mouse" "-")
((((((triple11) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The cat chases the rabbit.
True
6
proof
[(((triple11 ((((((triple11) -> rule1)) -> rule7)) -> rule6)) -> rule2) OR ((triple8 ((((((triple8) -> rule1)) -> rule7)) -> rule6)) -> rule2))]
("cat" "chases" "rabbit" "+")
((triple11 ((((((triple11) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((triple8 ((((((triple8) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The cat does not chase the rabbit.
False
6
inv-proof
[(((triple11 ((((((triple11) -> rule1)) -> rule7)) -> rule6)) -> rule2) OR ((triple8 ((((((triple8) -> rule1)) -> rule7)) -> rule6)) -> rule2))]
("cat" "chases" "rabbit" "-")
((triple11 ((((((triple11) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((triple8 ((((((triple8) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The cat likes the mouse.
True
7
proof
[(((((triple11 ((((((triple11) -> rule1)) -> rule7)) -> rule6)) -> rule2)) -> rule6) OR ((((triple8 ((((((triple8) -> rule1)) -> rule7)) -> rule6)) -> rule2)) -> rule6))]
("cat" "likes" "mouse" "+")
((((triple11 ((((((triple11) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int4
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int5
((((triple8 ((((((triple8) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5
The cat does not like the mouse.
False
7
inv-proof
[(((((triple11 ((((((triple11) -> rule1)) -> rule7)) -> rule6)) -> rule2)) -> rule6) OR ((((triple8 ((((((triple8) -> rule1)) -> rule7)) -> rule6)) -> rule2)) -> rule6))]
("cat" "likes" "mouse" "-")
((((triple11 ((((((triple11) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int4
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int5
((((triple8 ((((((triple8) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "cold" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "+")
The rabbit does not visit the mouse.
Unknown
inv-rconc
[@1: The rabbit visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "mouse" "-")
The lion chases the cat.
Unknown
rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "cat" "+")
The lion does not visit the mouse.
Unknown
inv-rconc
[@1: The lion visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "mouse" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat does not visit the rabbit.
Unknown
inv-random
[@0: The cat visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "rabbit" "-")
The mouse likes the lion.
Unknown
random
[@0: The mouse likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "lion" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat is rough.[(triple1)] The cat likes the rabbit.[(triple2)] The lion is rough.[(triple3)] The lion likes the mouse.[(triple4)] The mouse does not visit the rabbit.[(triple9)] The mouse is rough.[(triple5)] The mouse likes the cat.[(triple6)] The mouse likes the rabbit.[(triple7)] The mouse visits the cat.[(triple8)] The rabbit is rough.[(triple10)] The rabbit visits the cat.[(triple11)] @1: The mouse chases the cat.[(((triple8) -> rule1))] The rabbit chases the cat.[(((triple11) -> rule1))] @2: The mouse chases the rabbit.[(((((triple8) -> rule1)) -> rule7))] The rabbit chases the rabbit.[(((((triple11) -> rule1)) -> rule7))] @3: The mouse likes the mouse.[(((((((triple8) -> rule1)) -> rule7)) -> rule6))] The rabbit likes the mouse.[(((((((triple11) -> rule1)) -> rule7)) -> rule6))] @4: The cat chases the rabbit.[(((triple11 ((((((triple11) -> rule1)) -> rule7)) -> rule6)) -> rule2) OR ((triple8 ((((((triple8) -> rule1)) -> rule7)) -> rule6)) -> rule2))] @5: The cat likes the mouse.[(((((triple11 ((((((triple11) -> rule1)) -> rule7)) -> rule6)) -> rule2)) -> rule6) OR ((((triple8 ((((((triple8) -> rule1)) -> rule7)) -> rule6)) -> rule2)) -> rule6))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple4
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple6
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple7
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple11
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple8) -> (rule1 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
((triple11) -> (rule1 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((triple8) -> (rule1 % int2))) -> (rule7 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple11) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple8) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((((triple11) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple11 ((((((triple11) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((triple8 ((((((triple8) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((((triple11 ((((((triple11) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int4
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int5
((((triple8 ((((((triple8) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5