The cow is big. The cow needs the tiger. The mouse is blue. The mouse sees the tiger. The rabbit sees the mouse. The tiger is blue. The tiger needs the rabbit. If something needs the tiger then it does not visit the tiger. If something sees the mouse then the mouse sees the cow. If something is nice then it sees the rabbit. If the mouse visits the tiger and the tiger is young then the tiger sees the rabbit. If something needs the rabbit then it visits the cow. If something is young then it sees the cow. If something sees the cow then it needs the rabbit. If the tiger is big then the tiger is blue. If something visits the cow and it sees the cow then the cow needs the rabbit.
The cow is big.
("cow" "is" "big" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something needs the tiger then it does not visit the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "tiger" "-"))
If something sees the mouse then the mouse sees the cow.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If something is nice then it sees the rabbit.
((("something" "is" "nice" "+")) -> ("something" "sees" "rabbit" "+"))
If the mouse visits the tiger and the tiger is young then the tiger sees the rabbit.
((("mouse" "visits" "tiger" "+") ("tiger" "is" "young" "+")) -> ("tiger" "sees" "rabbit" "+"))
If something needs the rabbit then it visits the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "visits" "cow" "+"))
If something is young then it sees the cow.
((("something" "is" "young" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then it needs the rabbit.
((("something" "sees" "cow" "+")) -> ("something" "needs" "rabbit" "+"))
If the tiger is big then the tiger is blue.
((("tiger" "is" "big" "+")) -> ("tiger" "is" "blue" "+"))
If something visits the cow and it sees the cow then the cow needs the rabbit.
((("something" "visits" "cow" "+") ("something" "sees" "cow" "+")) -> ("cow" "needs" "rabbit" "+"))
The mouse is blue.
True
1
proof
[(triple3)]
("mouse" "is" "blue" "+")
triple3
The tiger does not need the rabbit.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "rabbit" "-")
triple7
The tiger visits the cow.
True
2
proof
[(((triple7) -> rule5))]
("tiger" "visits" "cow" "+")
((triple7) -> (rule5 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The mouse does not see the cow.
False
2
inv-proof
[(((triple5) -> rule2))]
("mouse" "sees" "cow" "-")
((triple5) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the rabbit.
True
3
proof
[(((((triple5) -> rule2)) -> rule7))]
("mouse" "needs" "rabbit" "+")
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse does not need the rabbit.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule7))]
("mouse" "needs" "rabbit" "-")
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse visits the cow.
True
4
proof
[(((((((triple5) -> rule2)) -> rule7)) -> rule5))]
("mouse" "visits" "cow" "+")
((((((triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse does not visit the cow.
False
4
inv-proof
[(((((((triple5) -> rule2)) -> rule7)) -> rule5))]
("mouse" "visits" "cow" "-")
((((((triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The cow needs the rabbit.
True
7
proof
[(((((((((triple5) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule2)) -> rule9))]
("cow" "needs" "rabbit" "+")
((((((((triple5) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple5) -> (rule2 % int4))) -> (rule9 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int4
The cow does not need the rabbit.
False
7
inv-proof
[(((((((((triple5) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule2)) -> rule9))]
("cow" "needs" "rabbit" "-")
((((((((triple5) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple5) -> (rule2 % int4))) -> (rule9 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int4
The cow visits the cow.
True
8
proof
[(((((((((((triple5) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule2)) -> rule9)) -> rule5))]
("cow" "visits" "cow" "+")
((((((((((triple5) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((triple5) -> (rule2 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int5
The cow does not visit the cow.
False
8
inv-proof
[(((((((((((triple5) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule2)) -> rule9)) -> rule5))]
("cow" "visits" "cow" "-")
((((((((((triple5) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((triple5) -> (rule2 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int5
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "cow" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The mouse does not see the rabbit.
Unknown
inv-rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "rabbit" "-")
The rabbit visits the cow.
Unknown
rconc
[@3: The rabbit visits the cow.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule6 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The cow does not see the rabbit.
Unknown
inv-rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit needs the tiger.
Unknown
random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "+")
The cow does not see the tiger.
Unknown
inv-random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cow is big.[(triple1)] The cow needs the tiger.[(triple2)] The mouse is blue.[(triple3)] The mouse sees the tiger.[(triple4)] The rabbit sees the mouse.[(triple5)] The tiger is blue.[(triple6)] The tiger needs the rabbit.[(triple7)] @1: The cow does not visit the tiger.[(((triple2) -> rule1))] The mouse sees the cow.[(((triple5) -> rule2))] The tiger visits the cow.[(((triple7) -> rule5))] @2: The mouse needs the rabbit.[(((((triple5) -> rule2)) -> rule7))] @3: The mouse visits the cow.[(((((((triple5) -> rule2)) -> rule7)) -> rule5))] @4: The cow needs the rabbit.[(((((((((triple5) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule2)) -> rule9))] @5: The cow visits the cow.[(((((((((((triple5) -> rule2)) -> rule7)) -> rule5) ((triple5) -> rule2)) -> rule9)) -> rule5))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple7
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
((triple2) -> (rule1 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple5) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple7) -> (rule5 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((((((triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((((((((triple5) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) ((triple5) -> (rule2 % int4))) -> (rule9 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int4
The cow visits the cow.
("cow" "visits" "cow" "+")
((((((((((triple5) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) ((triple5) -> (rule2 % int5))) -> (rule9 % int2))) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int5