The cat chases the dog. The cat eats the cow. The cat eats the dog. The cat sees the mouse. The cow is rough. The cow sees the cat. The dog chases the cow. The mouse eats the dog. The mouse is big. The mouse is round. The mouse sees the cow. If something chases the dog and the dog is young then the dog eats the cow. All big things are young. If something chases the cow then the cow sees the mouse. If something is young then it chases the cat. If something eats the dog and it is kind then it sees the mouse. If something eats the cat then the cat is young. If the cat sees the cow then the cow is big. If something chases the cat and the cat chases the dog then the cat sees the cow. If something chases the cow and it chases the cat then it is young.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something chases the dog and the dog is young then the dog eats the cow.
((("something" "chases" "dog" "+") ("dog" "is" "young" "+")) -> ("dog" "eats" "cow" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something chases the cow then the cow sees the mouse.
((("something" "chases" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If something is young then it chases the cat.
((("something" "is" "young" "+")) -> ("something" "chases" "cat" "+"))
If something eats the dog and it is kind then it sees the mouse.
((("something" "eats" "dog" "+") ("something" "is" "kind" "+")) -> ("something" "sees" "mouse" "+"))
If something eats the cat then the cat is young.
((("something" "eats" "cat" "+")) -> ("cat" "is" "young" "+"))
If the cat sees the cow then the cow is big.
((("cat" "sees" "cow" "+")) -> ("cow" "is" "big" "+"))
If something chases the cat and the cat chases the dog then the cat sees the cow.
((("something" "chases" "cat" "+") ("cat" "chases" "dog" "+")) -> ("cat" "sees" "cow" "+"))
If something chases the cow and it chases the cat then it is young.
((("something" "chases" "cow" "+") ("something" "chases" "cat" "+")) -> ("something" "is" "young" "+"))
The mouse sees the cow.
True
1
proof
[(triple11)]
("mouse" "sees" "cow" "+")
triple11
The mouse is not big.
False
1
inv-proof
[(triple9)]
("mouse" "is" "big" "-")
triple9
The mouse is young.
True
2
proof
[(((triple9) -> rule2))]
("mouse" "is" "young" "+")
((triple9) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple9) -> rule2))]
("mouse" "is" "young" "-")
((triple9) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse chases the cat.
True
3
proof
[(((((triple9) -> rule2)) -> rule4))]
("mouse" "chases" "cat" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not chase the cat.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule4))]
("mouse" "chases" "cat" "-")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cat sees the cow.
True
5
proof
[(((((((triple9) -> rule2)) -> rule4) triple1) -> rule8))]
("cat" "sees" "cow" "+")
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat does not see the cow.
False
5
inv-proof
[(((((((triple9) -> rule2)) -> rule4) triple1) -> rule8))]
("cat" "sees" "cow" "-")
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cow is big.
True
6
proof
[(((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7))]
("cow" "is" "big" "+")
((((((((triple9) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The cow is not big.
False
6
inv-proof
[(((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7))]
("cow" "is" "big" "-")
((((((((triple9) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The cow is young.
True
7
proof
[(((((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7)) -> rule2))]
("cow" "is" "young" "+")
((((((((((triple9) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
int5
The cow is not young.
False
7
inv-proof
[(((((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7)) -> rule2))]
("cow" "is" "young" "-")
((((((((((triple9) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
int5
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cat chases the cat.
Unknown
rconc
[@2: The cat chases the cat.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("cat" "chases" "cat" "+")
The dog does not chase the cat.
Unknown
inv-rconc
[@2: The dog chases the cat.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("dog" "chases" "cat" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "young" "+")
The dog is not young.
Unknown
inv-rconc
[@3: The dog is young.[CWA. Example of deepest failure = (rule9 <- rule4 <- rule2 <- FAIL)]]
("dog" "is" "young" "-")
The dog eats the cow.
Unknown
rconc
[@4: The dog eats the cow.[CWA. Example of deepest failure = (rule1 <- rule9 <- rule4 <- rule2 <- FAIL)]]
("dog" "eats" "cow" "+")
The mouse does not eat the cow.
Unknown
inv-random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "-")
The cow chases the mouse.
Unknown
random
[@0: The cow chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "mouse" "+")
The cow does not eat the mouse.
Unknown
inv-random
[@0: The cow eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "mouse" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat chases the dog.[(triple1)] The cat eats the cow.[(triple2)] The cat eats the dog.[(triple3)] The cat sees the mouse.[(triple4)] The cow is rough.[(triple5)] The cow sees the cat.[(triple6)] The dog chases the cow.[(triple7)] The mouse eats the dog.[(triple8)] The mouse is big.[(triple9)] The mouse is round.[(triple10)] The mouse sees the cow.[(triple11)] @1: The cow sees the mouse.[(((triple7) -> rule3))] The mouse is young.[(((triple9) -> rule2))] @2: The mouse chases the cat.[(((((triple9) -> rule2)) -> rule4))] @3: The cat sees the cow.[(((((((triple9) -> rule2)) -> rule4) triple1) -> rule8))] @4: The cow is big.[(((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7))] @5: The cow is young.[(((((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7)) -> rule2))] @6: The cow chases the cat.[(((((((((((((triple9) -> rule2)) -> rule4) triple1) -> rule8)) -> rule7)) -> rule2)) -> rule4))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cat eats the dog.
("cat" "eats" "dog" "+")
triple3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
The cow sees the cat.
("cow" "sees" "cat" "+")
triple6
The dog chases the cow.
("dog" "chases" "cow" "+")
triple7
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple7) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple9) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cow is big.
("cow" "is" "big" "+")
((((((((triple9) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The cow is young.
("cow" "is" "young" "+")
((((((((((triple9) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
int5
The cow chases the cat.
("cow" "chases" "cat" "+")
((((((((((((triple9) -> (rule2 % int6))) -> (rule4 % int5)) triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int5
The mouse is young.
("mouse" "is" "young" "+")
int6