The cow is kind. The cow is nice. The cow likes the lion. The cow likes the mouse. The cow visits the mouse. The lion is big. The lion likes the mouse. The mouse visits the lion. The tiger eats the mouse. The tiger is nice. The tiger is red. The tiger likes the cow. The tiger likes the lion. The tiger visits the cow. If the mouse eats the cow and the mouse likes the tiger then the mouse likes the cow. If someone is nice then they are young. If someone eats the lion then they are big. If someone is young then they eat the mouse. If someone eats the lion and they like the mouse then the lion likes the cow. All kind, big people are red. If someone eats the mouse and they are kind then the mouse is nice.
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If the mouse eats the cow and the mouse likes the tiger then the mouse likes the cow.
((("mouse" "eats" "cow" "+") ("mouse" "likes" "tiger" "+")) -> ("mouse" "likes" "cow" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone eats the lion then they are big.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they eat the mouse.
((("someone" "is" "young" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the lion and they like the mouse then the lion likes the cow.
((("someone" "eats" "lion" "+") ("someone" "likes" "mouse" "+")) -> ("lion" "likes" "cow" "+"))
All kind, big people are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone eats the mouse and they are kind then the mouse is nice.
((("someone" "eats" "mouse" "+") ("someone" "is" "kind" "+")) -> ("mouse" "is" "nice" "+"))
The tiger eats the mouse.
True
1
proof
[(triple9 OR ((((triple10) -> rule2)) -> rule4))]
("tiger" "eats" "mouse" "+")
triple9
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger does not like the cow.
False
1
inv-proof
[(triple12)]
("tiger" "likes" "cow" "-")
triple12
The cow is young.
True
2
proof
[(((triple2) -> rule2))]
("cow" "is" "young" "+")
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is not young.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "is" "young" "-")
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow eats the mouse.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("cow" "eats" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow does not eat the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("cow" "eats" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The mouse is nice.
True
5
proof
[(((((((triple2) -> rule2)) -> rule4) triple1) -> rule7))]
("mouse" "is" "nice" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The mouse is not nice.
False
5
inv-proof
[(((((((triple2) -> rule2)) -> rule4) triple1) -> rule7))]
("mouse" "is" "nice" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The mouse is young.
True
6
proof
[(((((((((triple2) -> rule2)) -> rule4) triple1) -> rule7)) -> rule2))]
("mouse" "is" "young" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The mouse is not young.
False
6
inv-proof
[(((((((((triple2) -> rule2)) -> rule4) triple1) -> rule7)) -> rule2))]
("mouse" "is" "young" "-")
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The mouse eats the mouse.
True
7
proof
[(((((((((((triple2) -> rule2)) -> rule4) triple1) -> rule7)) -> rule2)) -> rule4))]
("mouse" "eats" "mouse" "+")
((((((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5
The mouse does not eat the mouse.
False
7
inv-proof
[(((((((((((triple2) -> rule2)) -> rule4) triple1) -> rule7)) -> rule2)) -> rule4))]
("mouse" "eats" "mouse" "-")
((((((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "red" "-")
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 young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "young" "-")
The cow is red.
Unknown
rconc
[@2: The cow is red.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("cow" "is" "red" "+")
The lion does not eat the mouse.
Unknown
inv-rconc
[@2: The lion eats the mouse.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("lion" "eats" "mouse" "-")
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 like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The tiger does not eat the lion.
Unknown
inv-random
[@0: The tiger eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "lion" "-")
The lion visits the mouse.
Unknown
random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion visits the tiger.
Unknown
random
[@0: The lion visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "tiger" "+")
@0: The cow is kind.[(triple1)] The cow is nice.[(triple2)] The cow likes the lion.[(triple3)] The cow likes the mouse.[(triple4)] The cow visits the mouse.[(triple5)] The lion is big.[(triple6)] The lion likes the mouse.[(triple7)] The mouse visits the lion.[(triple8)] The tiger eats the mouse.[(triple9 OR ((((triple10) -> rule2)) -> rule4))] The tiger is nice.[(triple10)] The tiger is red.[(triple11)] The tiger likes the cow.[(triple12)] The tiger likes the lion.[(triple13)] The tiger visits the cow.[(triple14)] @1: The cow is young.[(((triple2) -> rule2))] The tiger is young.[(((triple10) -> rule2))] @2: The cow eats the mouse.[(((((triple2) -> rule2)) -> rule4))] @3: The mouse is nice.[(((((((triple2) -> rule2)) -> rule4) triple1) -> rule7))] @4: The mouse is young.[(((((((((triple2) -> rule2)) -> rule4) triple1) -> rule7)) -> rule2))] @5: The mouse eats the mouse.[(((((((((((triple2) -> rule2)) -> rule4) triple1) -> rule7)) -> rule2)) -> rule4))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple4
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple7
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple8
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple9
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple13
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple14
The cow is young.
("cow" "is" "young" "+")
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple10) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int4
The cow is young.
("cow" "is" "young" "+")
int5