The cat eats the tiger. The cat is rough. The lion eats the cat. The mouse chases the cat. The mouse chases the lion. The mouse is rough. The tiger chases the mouse. If the lion eats the tiger then the lion is green. If someone chases the tiger then the tiger chases the mouse. If someone is green and rough then they eat the tiger. Green people are young. If the mouse chases the lion then the lion eats the tiger. If someone sees the lion then the lion is cold.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is rough.
("cat" "is" "rough" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
If the lion eats the tiger then the lion is green.
((("lion" "eats" "tiger" "+")) -> ("lion" "is" "green" "+"))
If someone chases the tiger then the tiger chases the mouse.
((("someone" "chases" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone is green and rough then they eat the tiger.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "eats" "tiger" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If the mouse chases the lion then the lion eats the tiger.
((("mouse" "chases" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
If someone sees the lion then the lion is cold.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "cold" "+"))
The cat is rough.
True
1
proof
[(triple2)]
("cat" "is" "rough" "+")
triple2
The cat does not eat the tiger.
False
1
inv-proof
[(triple1)]
("cat" "eats" "tiger" "-")
triple1
The lion eats the tiger.
True
2
proof
[(((triple5) -> rule5))]
("lion" "eats" "tiger" "+")
((triple5) -> (rule5 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion does not eat the tiger.
False
2
inv-proof
[(((triple5) -> rule5))]
("lion" "eats" "tiger" "-")
((triple5) -> (rule5 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion is green.
True
3
proof
[(((((triple5) -> rule5)) -> rule1))]
("lion" "is" "green" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion is not green.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule1))]
("lion" "is" "green" "-")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion is young.
True
4
proof
[(((((((triple5) -> rule5)) -> rule1)) -> rule4))]
("lion" "is" "young" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion is not young.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule1)) -> rule4))]
("lion" "is" "young" "-")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "cold" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "young" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The mouse eats the tiger.
Unknown
rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "tiger" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat eats the tiger.[(triple1)] The cat is rough.[(triple2)] The lion eats the cat.[(triple3)] The mouse chases the cat.[(triple4)] The mouse chases the lion.[(triple5)] The mouse is rough.[(triple6)] The tiger chases the mouse.[(triple7)] @1: The lion eats the tiger.[(((triple5) -> rule5))] @2: The lion is green.[(((((triple5) -> rule5)) -> rule1))] @3: The lion is young.[(((((((triple5) -> rule5)) -> rule1)) -> rule4))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The lion eats the cat.
("lion" "eats" "cat" "+")
triple3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple7
The lion eats the tiger.
("lion" "eats" "tiger" "+")
((triple5) -> (rule5 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3