The bald eagle chases the mouse. The bald eagle is kind. The cat is nice. The cat is round. The cat likes the mouse. The cow chases the mouse. The cow is cold. The mouse chases the cat. The mouse chases the cow. The mouse is rough. The mouse does not like the bald eagle. If something chases the mouse then it likes the cow. If something is rough and it likes the bald eagle then it is round. If something likes the cow then it is round. If the cow sees the cat then the cat chases the mouse. If something is kind then it does not see the mouse. If something likes the cow and the cow is round then it sees the cat. If something sees the mouse then the mouse chases the cow. If the bald eagle is round then the bald eagle sees the cow. If something chases the cat then it is rough.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse does not like the bald eagle.
("mouse" "likes" "bald eagle" "-")
If something chases the mouse then it likes the cow.
((("something" "chases" "mouse" "+")) -> ("something" "likes" "cow" "+"))
If something is rough and it likes the bald eagle then it is round.
((("something" "is" "rough" "+") ("something" "likes" "bald eagle" "+")) -> ("something" "is" "round" "+"))
If something likes the cow then it is round.
((("something" "likes" "cow" "+")) -> ("something" "is" "round" "+"))
If the cow sees the cat then the cat chases the mouse.
((("cow" "sees" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If something is kind then it does not see the mouse.
((("something" "is" "kind" "+")) -> ("something" "sees" "mouse" "-"))
If something likes the cow and the cow is round then it sees the cat.
((("something" "likes" "cow" "+") ("cow" "is" "round" "+")) -> ("something" "sees" "cat" "+"))
If something sees the mouse then the mouse chases the cow.
((("something" "sees" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
If the bald eagle is round then the bald eagle sees the cow.
((("bald eagle" "is" "round" "+")) -> ("bald eagle" "sees" "cow" "+"))
If something chases the cat then it is rough.
((("something" "chases" "cat" "+")) -> ("something" "is" "rough" "+"))
The cat is round.
True
1
proof
[(triple4 OR ((((((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4)) -> rule1)) -> rule3))]
("cat" "is" "round" "+")
triple4
((((((((((triple6) -> (rule1 % int6)) ((((triple6) -> (rule1 % int6))) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
int4
The cow is round.
("cow" "is" "round" "+")
int5
The cow likes the cow.
("cow" "likes" "cow" "+")
int6
The cat does not like the mouse.
False
1
inv-proof
[(triple5)]
("cat" "likes" "mouse" "-")
triple5
The cow likes the cow.
True
2
proof
[(((triple6) -> rule1))]
("cow" "likes" "cow" "+")
((triple6) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The bald eagle sees the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("bald eagle" "sees" "mouse" "+")
((triple2) -> (rule5 % int1))
The bald eagle does not see the mouse.
("bald eagle" "sees" "mouse" "-")
int1
The cow is round.
True
3
proof
[(((((triple6) -> rule1)) -> rule3))]
("cow" "is" "round" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The bald eagle is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("bald eagle" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The cow sees the cat.
True
6
proof
[(((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6))]
("cow" "sees" "cat" "+")
((((triple6) -> (rule1 % int3)) ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow does not see the cat.
False
6
inv-proof
[(((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6))]
("cow" "sees" "cat" "-")
((((triple6) -> (rule1 % int3)) ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cat chases the mouse.
True
7
proof
[(((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4))]
("cat" "chases" "mouse" "+")
((((((triple6) -> (rule1 % int4)) ((((triple6) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
The cat does not chase the mouse.
False
7
inv-proof
[(((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4))]
("cat" "chases" "mouse" "-")
((((((triple6) -> (rule1 % int4)) ((((triple6) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
The cat likes the cow.
True
8
proof
[(((((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4)) -> rule1))]
("cat" "likes" "cow" "+")
((((((((triple6) -> (rule1 % int5)) ((((triple6) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cat does not like the cow.
False
8
inv-proof
[(((((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4)) -> rule1))]
("cat" "likes" "cow" "-")
((((((((triple6) -> (rule1 % int5)) ((((triple6) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cat" "is" "rough" "-")
The mouse is round.
Unknown
rconc
[@2: The mouse is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("mouse" "is" "round" "+")
The bald eagle is not rough.
Unknown
inv-rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("bald eagle" "is" "rough" "-")
The mouse likes the cow.
Unknown
rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "cow" "+")
The mouse does not see the cat.
Unknown
inv-rconc
[@2: The mouse sees the cat.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("mouse" "sees" "cat" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "is" "rough" "+")
The cow does not see the mouse.
Unknown
inv-random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "-")
The cat sees the cow.
Unknown
random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "+")
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 cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bald eagle chases the mouse.[(triple1)] The bald eagle is kind.[(triple2)] The cat is nice.[(triple3)] The cat is round.[(triple4 OR ((((((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4)) -> rule1)) -> rule3))] The cat likes the mouse.[(triple5)] The cow chases the mouse.[(triple6)] The cow is cold.[(triple7)] The mouse chases the cat.[(triple8)] The mouse chases the cow.[(triple9)] The mouse does not like the bald eagle.[(triple11)] The mouse is rough.[(triple10 OR ((triple8) -> rule9))] @1: The bald eagle does not see the mouse.[(((triple2) -> rule5))] The bald eagle likes the cow.[(((triple1) -> rule1))] The cow likes the cow.[(((triple6) -> rule1))] @2: The bald eagle is round.[(((((triple1) -> rule1)) -> rule3))] The cow is round.[(((((triple6) -> rule1)) -> rule3))] @3: The bald eagle sees the cat.[(((((triple1) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6))] The bald eagle sees the cow.[(((((((triple1) -> rule1)) -> rule3)) -> rule8))] The cow sees the cat.[(((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6))] @4: The cat chases the mouse.[(((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4))] @5: The cat likes the cow.[(((((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4)) -> rule1))] @6: The cat sees the cat.[(((((((((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6)) -> rule4)) -> rule1) ((((triple6) -> rule1)) -> rule3)) -> rule6))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
((((((((((triple6) -> (rule1 % int6)) ((((triple6) -> (rule1 % int6))) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
int4
The cow is round.
("cow" "is" "round" "+")
int5
The cow likes the cow.
("cow" "likes" "cow" "+")
int6
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple5
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple6
The cow is cold.
("cow" "is" "cold" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple9
The mouse does not like the bald eagle.
("mouse" "likes" "bald eagle" "-")
triple11
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
((triple8) -> (rule9 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bald eagle does not see the mouse.
("bald eagle" "sees" "mouse" "-")
((triple2) -> (rule5 % int1))
The bald eagle does not see the mouse.
("bald eagle" "sees" "mouse" "-")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple6) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
((((triple1) -> (rule1 % int4)) ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int4
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The bald eagle is round.
("bald eagle" "is" "round" "+")
int2
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
((((triple6) -> (rule1 % int3)) ((((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((((((triple6) -> (rule1 % int4)) ((((triple6) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
The cat likes the cow.
("cat" "likes" "cow" "+")
((((((((triple6) -> (rule1 % int5)) ((((triple6) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cow sees the cat.
("cow" "sees" "cat" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((((((triple6) -> (rule1 % int6)) ((((triple6) -> (rule1 % int6))) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple6) -> (rule1 % int6))) -> (rule3 % int5))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
int4
The cow is round.
("cow" "is" "round" "+")
int5
The cow likes the cow.
("cow" "likes" "cow" "+")
int6