The squirrel is cold. The tiger likes the squirrel. If something is cold then it chases the tiger. If something chases the tiger then it is big.
The squirrel is cold.
("squirrel" "is" "cold" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If something is cold then it chases the tiger.
((("something" "is" "cold" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the tiger then it is big.
((("something" "chases" "tiger" "+")) -> ("something" "is" "big" "+"))
The tiger likes the squirrel.
True
1
proof
[(triple2)]
("tiger" "likes" "squirrel" "+")
triple2
The squirrel is not cold.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "cold" "-")
triple1
The squirrel chases the tiger.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "chases" "tiger" "+")
((triple1) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "chases" "tiger" "-")
((triple1) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("squirrel" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The squirrel is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("squirrel" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is big.
Unknown
rconc
[@2: The tiger is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("tiger" "is" "big" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not eat the squirrel.
Unknown
inv-random
[@0: The tiger eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "squirrel" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The squirrel is cold.[(triple1)] The tiger likes the squirrel.[(triple2)] @1: The squirrel chases the tiger.[(((triple1) -> rule1))] @2: The squirrel is big.[(((((triple1) -> rule1)) -> rule2))]
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((triple1) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2