The cat chases the cow. The cat does not chase the mouse. The cat chases the tiger. The cat is kind. The cat is nice. The cat sees the tiger. The cow is round. The mouse eats the cow. The mouse sees the cow. The tiger chases the cat. The tiger chases the cow. The tiger eats the cat. If something sees the mouse then the mouse is big. If something chases the mouse then it does not eat the mouse. If something sees the cow then the cow sees the mouse. If something is big then it eats the cat. If something chases the tiger and it does not eat the cow then the tiger is not blue. If something eats the cow and it eats the tiger then the cow does not chase the mouse. If something chases the mouse then the mouse is round. If the tiger eats the cat and the tiger is not blue then the tiger chases the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cow is round.
("cow" "is" "round" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
If something sees the mouse then the mouse is big.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something chases the mouse then it does not eat the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "eats" "mouse" "-"))
If something sees the cow then the cow sees the mouse.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If something is big then it eats the cat.
((("something" "is" "big" "+")) -> ("something" "eats" "cat" "+"))
If something chases the tiger and it does not eat the cow then the tiger is not blue.
((("something" "chases" "tiger" "+") ("something" "eats" "cow" "~")) -> ("tiger" "is" "blue" "-"))
If something eats the cow and it eats the tiger then the cow does not chase the mouse.
((("something" "eats" "cow" "+") ("something" "eats" "tiger" "+")) -> ("cow" "chases" "mouse" "-"))
If something chases the mouse then the mouse is round.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If the tiger eats the cat and the tiger is not blue then the tiger chases the cow.
((("tiger" "eats" "cat" "+") ("tiger" "is" "blue" "~")) -> ("tiger" "chases" "cow" "+"))
The cat chases the tiger.
True
1
proof
[(triple3)]
("cat" "chases" "tiger" "+")
triple3
The tiger does not eat the cat.
False
1
inv-proof
[(triple12)]
("tiger" "eats" "cat" "-")
triple12
The cow sees the mouse.
True
2
proof
[(((triple9) -> rule3))]
("cow" "sees" "mouse" "+")
((triple9) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow does not see the mouse.
False
2
inv-proof
[(((triple9) -> rule3))]
("cow" "sees" "mouse" "-")
((triple9) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse is big.
True
3
proof
[(((((triple9) -> rule3)) -> rule1))]
("mouse" "is" "big" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse is not big.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule1))]
("mouse" "is" "big" "-")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse eats the cat.
True
4
proof
[(((((((triple9) -> rule3)) -> rule1)) -> rule4))]
("mouse" "eats" "cat" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The mouse does not eat the cat.
False
4
inv-proof
[(((((((triple9) -> rule3)) -> rule1)) -> rule4))]
("mouse" "eats" "cat" "-")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cat" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cat" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "round" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
The mouse does not eat the tiger.
Unknown
inv-random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cat chases the cow.[(triple1)] The cat chases the tiger.[(triple3)] The cat does not chase the mouse.[(triple2)] The cat is kind.[(triple4)] The cat is nice.[(triple5)] The cat sees the tiger.[(triple6)] The cow is round.[(triple7)] The mouse eats the cow.[(triple8)] The mouse sees the cow.[(triple9)] The tiger chases the cat.[(triple10)] The tiger chases the cow.[(triple11)] The tiger eats the cat.[(triple12)] @1: The cow sees the mouse.[(((triple9) -> rule3))] @2: The mouse is big.[(((((triple9) -> rule3)) -> rule1))] @3: The mouse eats the cat.[(((((((triple9) -> rule3)) -> rule1)) -> rule4))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple3
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple6
The cow is round.
("cow" "is" "round" "+")
triple7
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple8
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple11
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple12
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple9) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3