The cow sees the dog. The cow sees the rabbit. The cow visits the mouse. The dog needs the mouse. The dog sees the mouse. The dog sees the rabbit. The dog visits the mouse. The mouse is blue. The mouse is not kind. The mouse needs the cow. The mouse sees the dog. The mouse sees the rabbit. The mouse does not visit the cow. The mouse visits the dog. The mouse visits the rabbit. The rabbit is blue. If the dog visits the cow and the cow sees the rabbit then the dog sees the cow. If something visits the cow and the cow needs the dog then the dog is rough. Blue things are young. If something visits the mouse then it is blue. If something is young then it sees the mouse. If something sees the cow then it is not kind. If something visits the mouse and it is kind then it needs the cow. If something needs the rabbit and it needs the dog then the rabbit needs the mouse. If the cow sees the mouse then the cow is kind.
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is not kind.
("mouse" "is" "kind" "-")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
If the dog visits the cow and the cow sees the rabbit then the dog sees the cow.
((("dog" "visits" "cow" "+") ("cow" "sees" "rabbit" "+")) -> ("dog" "sees" "cow" "+"))
If something visits the cow and the cow needs the dog then the dog is rough.
((("something" "visits" "cow" "+") ("cow" "needs" "dog" "+")) -> ("dog" "is" "rough" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something visits the mouse then it is blue.
((("something" "visits" "mouse" "+")) -> ("something" "is" "blue" "+"))
If something is young then it sees the mouse.
((("something" "is" "young" "+")) -> ("something" "sees" "mouse" "+"))
If something sees the cow then it is not kind.
((("something" "sees" "cow" "+")) -> ("something" "is" "kind" "-"))
If something visits the mouse and it is kind then it needs the cow.
((("something" "visits" "mouse" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "cow" "+"))
If something needs the rabbit and it needs the dog then the rabbit needs the mouse.
((("something" "needs" "rabbit" "+") ("something" "needs" "dog" "+")) -> ("rabbit" "needs" "mouse" "+"))
If the cow sees the mouse then the cow is kind.
((("cow" "sees" "mouse" "+")) -> ("cow" "is" "kind" "+"))
The dog visits the mouse.
True
1
proof
[(triple7)]
("dog" "visits" "mouse" "+")
triple7
The mouse does not need the cow.
False
1
inv-proof
[(triple10)]
("mouse" "needs" "cow" "-")
triple10
The mouse is young.
True
2
proof
[(((triple8) -> rule3))]
("mouse" "is" "young" "+")
((triple8) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("cow" "is" "blue" "-")
((triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The dog is young.
True
3
proof
[(((((triple7) -> rule4)) -> rule3))]
("dog" "is" "young" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The mouse does not see the mouse.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule5))]
("mouse" "sees" "mouse" "-")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cow sees the mouse.
True
4
proof
[(((((((triple3) -> rule4)) -> rule3)) -> rule5))]
("cow" "sees" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow does not see the mouse.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule3)) -> rule5))]
("cow" "sees" "mouse" "-")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is kind.
True
5
proof
[(((((((((triple3) -> rule4)) -> rule3)) -> rule5)) -> rule9))]
("cow" "is" "kind" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The cow is not kind.
False
5
inv-proof
[(((((((((triple3) -> rule4)) -> rule3)) -> rule5)) -> rule9))]
("cow" "is" "kind" "-")
((((((((triple3) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The cow needs the cow.
True
7
proof
[(((triple3 ((((((((triple3) -> rule4)) -> rule3)) -> rule5)) -> rule9)) -> rule7))]
("cow" "needs" "cow" "+")
((triple3 ((((((((triple3) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The cow does not need the cow.
False
7
inv-proof
[(((triple3 ((((((((triple3) -> rule4)) -> rule3)) -> rule5)) -> rule9)) -> rule7))]
("cow" "needs" "cow" "-")
((triple3 ((((((((triple3) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "rough" "-")
The dog sees the cow.
Unknown
rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "cow" "+")
The dog does not need the cow.
Unknown
inv-rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "needs" "cow" "-")
The rabbit needs the cow.
Unknown
rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "cow" "+")
The rabbit does not need the mouse.
Unknown
inv-rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit needs the dog.
Unknown
random
[@0: The rabbit needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "dog" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The cow needs the dog.
Unknown
random
[@0: The cow needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "dog" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
@0: The cow sees the dog.[(triple1)] The cow sees the rabbit.[(triple2)] The cow visits the mouse.[(triple3)] The dog needs the mouse.[(triple4)] The dog sees the mouse.[(triple5 OR ((((((triple7) -> rule4)) -> rule3)) -> rule5))] The dog sees the rabbit.[(triple6)] The dog visits the mouse.[(triple7)] The mouse does not visit the cow.[(triple13)] The mouse is blue.[(triple8)] The mouse is not kind.[(triple9)] The mouse needs the cow.[(triple10)] The mouse sees the dog.[(triple11)] The mouse sees the rabbit.[(triple12)] The mouse visits the dog.[(triple14)] The mouse visits the rabbit.[(triple15)] The rabbit is blue.[(triple16)] @1: The cow is blue.[(((triple3) -> rule4))] The dog is blue.[(((triple7) -> rule4))] The mouse is young.[(((triple8) -> rule3))] The rabbit is young.[(((triple16) -> rule3))] @2: The cow is young.[(((((triple3) -> rule4)) -> rule3))] The dog is young.[(((((triple7) -> rule4)) -> rule3))] The mouse sees the mouse.[(((((triple8) -> rule3)) -> rule5))] The rabbit sees the mouse.[(((((triple16) -> rule3)) -> rule5))] @3: The cow sees the mouse.[(((((((triple3) -> rule4)) -> rule3)) -> rule5))] @4: The cow is kind.[(((((((((triple3) -> rule4)) -> rule3)) -> rule5)) -> rule9))] @5: The cow needs the cow.[(((triple3 ((((((((triple3) -> rule4)) -> rule3)) -> rule5)) -> rule9)) -> rule7))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple6
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple7
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple13
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse is not kind.
("mouse" "is" "kind" "-")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple10
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple11
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple12
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple14
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple15
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple16
The cow is blue.
("cow" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((triple7) -> (rule4 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple8) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple16) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((((triple16) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
((((((((triple3) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple3 ((((((((triple3) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5