The cow does not see the tiger. The cow does not visit the lion. The lion is blue. The lion is green. The lion needs the cow. The lion does not need the mouse. The lion needs the tiger. The lion visits the cow. The mouse sees the cow. The mouse sees the lion. The mouse visits the tiger. The tiger needs the cow. The tiger needs the lion. The tiger sees the cow. The tiger visits the lion. The tiger visits the mouse. All green people are big. If someone visits the cow then they see the cow. If the tiger needs the lion and the tiger needs the cow then the tiger is green. If someone is big then they do not see the tiger. If someone visits the lion then the lion sees the cow. If the cow needs the lion then the lion sees the cow. If the cow visits the lion then the lion visits the cow. If someone is blue and not young then they need the lion.
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
The cow does not visit the lion.
("cow" "visits" "lion" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone visits the cow then they see the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If the tiger needs the lion and the tiger needs the cow then the tiger is green.
((("tiger" "needs" "lion" "+") ("tiger" "needs" "cow" "+")) -> ("tiger" "is" "green" "+"))
If someone is big then they do not see the tiger.
((("someone" "is" "big" "+")) -> ("someone" "sees" "tiger" "-"))
If someone visits the lion then the lion sees the cow.
((("someone" "visits" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If the cow needs the lion then the lion sees the cow.
((("cow" "needs" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If the cow visits the lion then the lion visits the cow.
((("cow" "visits" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If someone is blue and not young then they need the lion.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "needs" "lion" "+"))
The tiger visits the lion.
True
1
proof
[(triple15)]
("tiger" "visits" "lion" "+")
triple15
The lion does not visit the cow.
False
1
inv-proof
[(triple8)]
("lion" "visits" "cow" "-")
triple8
The lion is big.
True
2
proof
[(((triple4) -> rule1))]
("lion" "is" "big" "+")
((triple4) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "is" "big" "-")
((triple4) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The tiger is big.
True
4
proof
[(((((triple13 triple12) -> rule3)) -> rule1))]
("tiger" "is" "big" "+")
((((triple13 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The lion sees the tiger.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("lion" "sees" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The tiger does not see the tiger.
True
5
proof
[(((((((triple13 triple12) -> rule3)) -> rule1)) -> rule4))]
("tiger" "sees" "tiger" "-")
((((((triple13 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger sees the tiger.
False
5
inv-proof
[(((((((triple13 triple12) -> rule3)) -> rule1)) -> rule4))]
("tiger" "sees" "tiger" "+")
((((((triple13 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "lion" "-")
The mouse needs the lion.
Unknown
rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "needs" "lion" "+")
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "cow" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not need the mouse.
Unknown
inv-random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "-")
The mouse visits the lion.
Unknown
random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "+")
@0: The cow does not see the tiger.[(triple1)] The cow does not visit the lion.[(triple2)] The lion does not need the mouse.[(triple6)] The lion is blue.[(triple3)] The lion is green.[(triple4)] The lion needs the cow.[(triple5)] The lion needs the tiger.[(triple7)] The lion visits the cow.[(triple8)] The mouse sees the cow.[(triple9)] The mouse sees the lion.[(triple10)] The mouse visits the tiger.[(triple11)] The tiger needs the cow.[(triple12)] The tiger needs the lion.[(triple13)] The tiger sees the cow.[(triple14)] The tiger visits the lion.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The lion is big.[(((triple4) -> rule1))] The lion sees the cow.[(((triple15) -> rule5) OR ((triple8) -> rule2))] The tiger is green.[(((triple13 triple12) -> rule3))] @2: The lion does not see the tiger.[(((((triple4) -> rule1)) -> rule4))] The tiger is big.[(((((triple13 triple12) -> rule3)) -> rule1))] @3: The tiger does not see the tiger.[(((((((triple13 triple12) -> rule3)) -> rule1)) -> rule4))]
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
triple1
The cow does not visit the lion.
("cow" "visits" "lion" "-")
triple2
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
triple6
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion needs the cow.
("lion" "needs" "cow" "+")
triple5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple7
The lion visits the cow.
("lion" "visits" "cow" "+")
triple8
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple11
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple12
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple13
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The lion is big.
("lion" "is" "big" "+")
((triple4) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple15) -> (rule5 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
((triple8) -> (rule2 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple13 triple12) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((triple13 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
((((((triple13 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3