The cat is rough. The cat does not visit the dog. The cat does not visit the rabbit. The dog chases the cat. The dog chases the rabbit. The dog is not red. The dog is round. The mouse chases the dog. The mouse is not rough. The rabbit sees the mouse. If someone chases the dog and the dog visits the rabbit then the rabbit chases the cat. If someone is round then they do not see the mouse. If someone sees the mouse then the mouse sees the cat. If the dog sees the mouse then the dog chases the rabbit. If someone sees the dog and the dog chases the rabbit then the rabbit is young. If someone sees the rabbit and the rabbit chases the cat then the cat is red. If someone is young then they see the cat. If someone sees the cat then they see the dog.
The cat is rough.
("cat" "is" "rough" "+")
The cat does not visit the dog.
("cat" "visits" "dog" "-")
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is not red.
("dog" "is" "red" "-")
The dog is round.
("dog" "is" "round" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone chases the dog and the dog visits the rabbit then the rabbit chases the cat.
((("someone" "chases" "dog" "+") ("dog" "visits" "rabbit" "+")) -> ("rabbit" "chases" "cat" "+"))
If someone is round then they do not see the mouse.
((("someone" "is" "round" "+")) -> ("someone" "sees" "mouse" "-"))
If someone sees the mouse then the mouse sees the cat.
((("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If the dog sees the mouse then the dog chases the rabbit.
((("dog" "sees" "mouse" "+")) -> ("dog" "chases" "rabbit" "+"))
If someone sees the dog and the dog chases the rabbit then the rabbit is young.
((("someone" "sees" "dog" "+") ("dog" "chases" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone sees the rabbit and the rabbit chases the cat then the cat is red.
((("someone" "sees" "rabbit" "+") ("rabbit" "chases" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone is young then they see the cat.
((("someone" "is" "young" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat then they see the dog.
((("someone" "sees" "cat" "+")) -> ("someone" "sees" "dog" "+"))
The dog chases the rabbit.
True
1
proof
[(triple5)]
("dog" "chases" "rabbit" "+")
triple5
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The mouse sees the cat.
True
2
proof
[(((triple10) -> rule3))]
("mouse" "sees" "cat" "+")
((triple10) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The dog sees the mouse.
False
2
inv-proof
[(((triple7) -> rule2))]
("dog" "sees" "mouse" "+")
((triple7) -> (rule2 % int1))
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
int1
The mouse sees the dog.
True
3
proof
[(((((triple10) -> rule3)) -> rule8))]
("mouse" "sees" "dog" "+")
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse does not see the dog.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule8))]
("mouse" "sees" "dog" "-")
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The rabbit is young.
True
5
proof
[(((((((triple10) -> rule3)) -> rule8) triple5) -> rule5))]
("rabbit" "is" "young" "+")
((((((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The rabbit is not young.
False
5
inv-proof
[(((((((triple10) -> rule3)) -> rule8) triple5) -> rule5))]
("rabbit" "is" "young" "-")
((((((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The rabbit sees the cat.
True
6
proof
[(((((((((triple10) -> rule3)) -> rule8) triple5) -> rule5)) -> rule7))]
("rabbit" "sees" "cat" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule8 % int3)) triple5) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The rabbit does not see the cat.
False
6
inv-proof
[(((((((((triple10) -> rule3)) -> rule8) triple5) -> rule5)) -> rule7))]
("rabbit" "sees" "cat" "-")
((((((((triple10) -> (rule3 % int4))) -> (rule8 % int3)) triple5) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The rabbit sees the dog.
True
7
proof
[(((((((((((triple10) -> rule3)) -> rule8) triple5) -> rule5)) -> rule7)) -> rule8))]
("rabbit" "sees" "dog" "+")
((((((((((triple10) -> (rule3 % int5))) -> (rule8 % int4)) triple5) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int5
The rabbit does not see the dog.
False
7
inv-proof
[(((((((((((triple10) -> rule3)) -> rule8) triple5) -> rule5)) -> rule7)) -> rule8))]
("rabbit" "sees" "dog" "-")
((((((((((triple10) -> (rule3 % int5))) -> (rule8 % int4)) triple5) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int5
The cat does not see the dog.
Unknown
inv-rconc
[@2: The cat sees the dog.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("cat" "sees" "dog" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "sees" "cat" "+")
The rabbit does not chase the cat.
Unknown
inv-rconc
[@1: The rabbit chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "cat" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "red" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@2: The dog sees the dog.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("dog" "sees" "dog" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The cat does not see the rabbit.
Unknown
inv-random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The mouse visits the rabbit.
Unknown
random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "+")
@0: The cat does not visit the dog.[(triple2)] The cat does not visit the rabbit.[(triple3)] The cat is rough.[(triple1)] The dog chases the cat.[(triple4)] The dog chases the rabbit.[(triple5)] The dog is not red.[(triple6)] The dog is round.[(triple7)] The mouse chases the dog.[(triple8)] The mouse is not rough.[(triple9)] The rabbit sees the mouse.[(triple10)] @1: The dog does not see the mouse.[(((triple7) -> rule2))] The mouse sees the cat.[(((triple10) -> rule3))] @2: The mouse sees the dog.[(((((triple10) -> rule3)) -> rule8))] @3: The rabbit is young.[(((((((triple10) -> rule3)) -> rule8) triple5) -> rule5))] @4: The rabbit sees the cat.[(((((((((triple10) -> rule3)) -> rule8) triple5) -> rule5)) -> rule7))] @5: The rabbit sees the dog.[(((((((((((triple10) -> rule3)) -> rule8) triple5) -> rule5)) -> rule7)) -> rule8))]
The cat does not visit the dog.
("cat" "visits" "dog" "-")
triple2
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple1
The dog chases the cat.
("dog" "chases" "cat" "+")
triple4
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple5
The dog is not red.
("dog" "is" "red" "-")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple8
The mouse is not rough.
("mouse" "is" "rough" "-")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
((triple7) -> (rule2 % int1))
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple10) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((((((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule8 % int3)) triple5) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((((((((triple10) -> (rule3 % int5))) -> (rule8 % int4)) triple5) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int4
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int5