The cat chases the tiger. The cat is blue. The cat is nice. The cat does not visit the mouse. The mouse chases the cat. The mouse chases the rabbit. The mouse chases the tiger. The mouse eats the tiger. The mouse is red. The mouse does not visit the rabbit. The rabbit does not eat the tiger. The rabbit is rough. The tiger chases the mouse. The tiger chases the rabbit. The tiger visits the cat. If something eats the rabbit and the rabbit is blue then it eats the tiger. If something is red then it chases the cat. If something eats the rabbit then the rabbit chases the tiger. If the cat eats the mouse and the rabbit does not visit the cat then the rabbit chases the tiger. If something eats the cat then it visits the rabbit. If something chases the mouse and it eats the tiger then the tiger visits the mouse. If something chases the tiger then it eats the rabbit. If something chases the mouse and the mouse does not chase the cat then the cat is not nice.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something eats the rabbit and the rabbit is blue then it eats the tiger.
((("something" "eats" "rabbit" "+") ("rabbit" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something is red then it chases the cat.
((("something" "is" "red" "+")) -> ("something" "chases" "cat" "+"))
If something eats the rabbit then the rabbit chases the tiger.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "+"))
If the cat eats the mouse and the rabbit does not visit the cat then the rabbit chases the tiger.
((("cat" "eats" "mouse" "+") ("rabbit" "visits" "cat" "~")) -> ("rabbit" "chases" "tiger" "+"))
If something eats the cat then it visits the rabbit.
((("something" "eats" "cat" "+")) -> ("something" "visits" "rabbit" "+"))
If something chases the mouse and it eats the tiger then the tiger visits the mouse.
((("something" "chases" "mouse" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If something chases the tiger then it eats the rabbit.
((("something" "chases" "tiger" "+")) -> ("something" "eats" "rabbit" "+"))
If something chases the mouse and the mouse does not chase the cat then the cat is not nice.
((("something" "chases" "mouse" "+") ("mouse" "chases" "cat" "~")) -> ("cat" "is" "nice" "-"))
The tiger chases the mouse.
True
1
proof
[(triple13)]
("tiger" "chases" "mouse" "+")
triple13
The cat does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cat" "chases" "tiger" "-")
triple1
The mouse eats the rabbit.
True
2
proof
[(((triple7) -> rule7))]
("mouse" "eats" "rabbit" "+")
((triple7) -> (rule7 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse does not eat the rabbit.
False
2
inv-proof
[(((triple7) -> rule7))]
("mouse" "eats" "rabbit" "-")
((triple7) -> (rule7 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
True
3
proof
[(((((triple1) -> rule7)) -> rule3) OR ((((triple7) -> rule7)) -> rule3))]
("rabbit" "chases" "tiger" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The rabbit does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3) OR ((((triple7) -> rule7)) -> rule3))]
("rabbit" "chases" "tiger" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The rabbit eats the rabbit.
True
4
proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule7) OR ((((((triple7) -> rule7)) -> rule3)) -> rule7))]
("rabbit" "eats" "rabbit" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int3
The rabbit does not eat the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule7) OR ((((((triple7) -> rule7)) -> rule3)) -> rule7))]
("rabbit" "eats" "rabbit" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int3
The tiger does not eat the rabbit.
Unknown
inv-rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "eats" "rabbit" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "cat" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger visits the mouse.
Unknown
rconc
[@2: The tiger visits the mouse.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("tiger" "visits" "mouse" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat chases the tiger.[(triple1)] The cat does not visit the mouse.[(triple4)] The cat is blue.[(triple2)] The cat is nice.[(triple3)] The mouse chases the cat.[(triple5 OR ((triple9) -> rule2))] The mouse chases the rabbit.[(triple6)] The mouse chases the tiger.[(triple7)] The mouse does not visit the rabbit.[(triple10)] The mouse eats the tiger.[(triple8)] The mouse is red.[(triple9)] The rabbit does not eat the tiger.[(triple11)] The rabbit is rough.[(triple12)] The tiger chases the mouse.[(triple13)] The tiger chases the rabbit.[(triple14)] The tiger visits the cat.[(triple15)] @1: The cat eats the rabbit.[(((triple1) -> rule7))] The mouse eats the rabbit.[(((triple7) -> rule7))] @2: The rabbit chases the tiger.[(((((triple1) -> rule7)) -> rule3) OR ((((triple7) -> rule7)) -> rule3))] @3: The rabbit eats the rabbit.[(((((((triple1) -> rule7)) -> rule3)) -> rule7) OR ((((((triple7) -> rule7)) -> rule3)) -> rule7))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
triple4
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple5
((triple9) -> (rule2 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple6
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple7
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple10
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple8
The mouse is red.
("mouse" "is" "red" "+")
triple9
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple13
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple14
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((triple1) -> (rule7 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
((triple7) -> (rule7 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int2
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int3