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