The cat is not young. The cow is cold. The lion sees the mouse. The mouse does not visit the cow. If something needs the mouse and the mouse visits the lion then the lion sees the cat. If something visits the cow then the cow visits the lion. If something needs the cat then the cat does not need the mouse. If something is kind then it is blue. If something visits the lion then it is not blue. If something is blue and not young then it does not visit the cat. If something needs the mouse then it visits the cow. If something sees the mouse then it needs the mouse.
The cat is not young.
("cat" "is" "young" "-")
The cow is cold.
("cow" "is" "cold" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
If something needs the mouse and the mouse visits the lion then the lion sees the cat.
((("something" "needs" "mouse" "+") ("mouse" "visits" "lion" "+")) -> ("lion" "sees" "cat" "+"))
If something visits the cow then the cow visits the lion.
((("something" "visits" "cow" "+")) -> ("cow" "visits" "lion" "+"))
If something needs the cat then the cat does not need the mouse.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "mouse" "-"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something visits the lion then it is not blue.
((("something" "visits" "lion" "+")) -> ("something" "is" "blue" "-"))
If something is blue and not young then it does not visit the cat.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "visits" "cat" "-"))
If something needs the mouse then it visits the cow.
((("something" "needs" "mouse" "+")) -> ("something" "visits" "cow" "+"))
If something sees the mouse then it needs the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
The mouse does not visit the cow.
True
1
proof
[(triple4)]
("mouse" "visits" "cow" "-")
triple4
The lion does not see the mouse.
False
1
inv-proof
[(triple3)]
("lion" "sees" "mouse" "-")
triple3
The lion needs the mouse.
True
2
proof
[(((triple3) -> rule8))]
("lion" "needs" "mouse" "+")
((triple3) -> (rule8 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule8))]
("lion" "needs" "mouse" "-")
((triple3) -> (rule8 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion visits the cow.
True
3
proof
[(((((triple3) -> rule8)) -> rule7))]
("lion" "visits" "cow" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion does not visit the cow.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule7))]
("lion" "visits" "cow" "-")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The cow visits the lion.
True
4
proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule2))]
("cow" "visits" "lion" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The cow does not visit the lion.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule2))]
("cow" "visits" "lion" "-")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The cow does not need the mouse.
Unknown
inv-rconc
[@1: The cow needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "needs" "mouse" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The cat visits the cow.
Unknown
rconc
[@2: The cat visits the cow.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("cat" "visits" "cow" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The cow needs the lion.
Unknown
random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "+")
The lion does not see the cow.
Unknown
inv-random
[@0: The lion sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cat is not young.[(triple1)] The cow is cold.[(triple2)] The lion sees the mouse.[(triple3)] The mouse does not visit the cow.[(triple4)] @1: The lion needs the mouse.[(((triple3) -> rule8))] @2: The lion visits the cow.[(((((triple3) -> rule8)) -> rule7))] @3: The cow visits the lion.[(((((((triple3) -> rule8)) -> rule7)) -> rule2))] @4: The cow is not blue.[(((((((((triple3) -> rule8)) -> rule7)) -> rule2)) -> rule5))]
The cat is not young.
("cat" "is" "young" "-")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple4
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple3) -> (rule8 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The cow is not blue.
("cow" "is" "blue" "-")
((((((((triple3) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int4