The cat chases the cow. The cat chases the mouse. The cat is cold. The cat is round. The cat is young. The cat likes the cow. The cow chases the cat. The cow chases the mouse. The cow is not big. The cow is cold. The cow is round. The cow is young. The cow likes the cat. The cow sees the cat. The mouse is round. The mouse likes the cow. If something chases the mouse and the mouse is big then the mouse sees the cow. If something sees the mouse then the mouse is big. If something sees the cat then the cat sees the mouse.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is not big.
("cow" "is" "big" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If something chases the mouse and the mouse is big then the mouse sees the cow.
((("something" "chases" "mouse" "+") ("mouse" "is" "big" "+")) -> ("mouse" "sees" "cow" "+"))
If something sees the mouse then the mouse is big.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something sees the cat then the cat sees the mouse.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
The cat likes the cow.
True
1
proof
[(triple6)]
("cat" "likes" "cow" "+")
triple6
The cow does not see the cat.
False
1
inv-proof
[(triple14)]
("cow" "sees" "cat" "-")
triple14
The cat sees the mouse.
True
2
proof
[(((triple14) -> rule3))]
("cat" "sees" "mouse" "+")
((triple14) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat does not see the mouse.
False
2
inv-proof
[(((triple14) -> rule3))]
("cat" "sees" "mouse" "-")
((triple14) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse is big.
True
3
proof
[(((((triple14) -> rule3)) -> rule2))]
("mouse" "is" "big" "+")
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse is not big.
False
3
inv-proof
[(((((triple14) -> rule3)) -> rule2))]
("mouse" "is" "big" "-")
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse sees the cow.
True
5
proof
[(((triple2 ((((triple14) -> rule3)) -> rule2)) -> rule1) OR ((triple8 ((((triple14) -> rule3)) -> rule2)) -> rule1))]
("mouse" "sees" "cow" "+")
((triple2 ((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
((triple8 ((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The mouse does not see the cow.
False
5
inv-proof
[(((triple2 ((((triple14) -> rule3)) -> rule2)) -> rule1) OR ((triple8 ((((triple14) -> rule3)) -> rule2)) -> rule1))]
("mouse" "sees" "cow" "-")
((triple2 ((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
((triple8 ((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The mouse does not like the cat.
Unknown
inv-random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "-")
The mouse chases the cat.
Unknown
random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "+")
The mouse does not chase the cow.
Unknown
inv-random
[@0: The mouse chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cow" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the cow.[(triple1)] The cat chases the mouse.[(triple2)] The cat is cold.[(triple3)] The cat is round.[(triple4)] The cat is young.[(triple5)] The cat likes the cow.[(triple6)] The cow chases the cat.[(triple7)] The cow chases the mouse.[(triple8)] The cow is cold.[(triple10)] The cow is not big.[(triple9)] The cow is round.[(triple11)] The cow is young.[(triple12)] The cow likes the cat.[(triple13)] The cow sees the cat.[(triple14)] The mouse is round.[(triple15)] The mouse likes the cow.[(triple16)] @1: The cat sees the mouse.[(((triple14) -> rule3))] @2: The mouse is big.[(((((triple14) -> rule3)) -> rule2))] @3: The mouse sees the cow.[(((triple2 ((((triple14) -> rule3)) -> rule2)) -> rule1) OR ((triple8 ((((triple14) -> rule3)) -> rule2)) -> rule1))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
The cow chases the cat.
("cow" "chases" "cat" "+")
triple7
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple8
The cow is cold.
("cow" "is" "cold" "+")
triple10
The cow is not big.
("cow" "is" "big" "-")
triple9
The cow is round.
("cow" "is" "round" "+")
triple11
The cow is young.
("cow" "is" "young" "+")
triple12
The cow likes the cat.
("cow" "likes" "cat" "+")
triple13
The cow sees the cat.
("cow" "sees" "cat" "+")
triple14
The mouse is round.
("mouse" "is" "round" "+")
triple15
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple16
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple14) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple2 ((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
((triple8 ((((triple14) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3