The cat visits the cow. The cow chases the lion. The lion chases the cow. The tiger eats the cow. If someone eats the cow then they are cold. If someone is green then they visit the lion. If someone is cold then they chase the lion.
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If someone eats the cow then they are cold.
((("someone" "eats" "cow" "+")) -> ("someone" "is" "cold" "+"))
If someone is green then they visit the lion.
((("someone" "is" "green" "+")) -> ("someone" "visits" "lion" "+"))
If someone is cold then they chase the lion.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "lion" "+"))
The tiger eats the cow.
True
1
proof
[(triple4)]
("tiger" "eats" "cow" "+")
triple4
The cow does not chase the lion.
False
1
inv-proof
[(triple2)]
("cow" "chases" "lion" "-")
triple2
The tiger is cold.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "is" "cold" "-")
((triple4) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger chases the lion.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("tiger" "chases" "lion" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger does not chase the lion.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("tiger" "chases" "lion" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The lion does not chase the lion.
Unknown
inv-rconc
[@2: The lion chases the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "chases" "lion" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "+")
The cat does not visit the lion.
Unknown
inv-rconc
[@1: The cat visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "lion" "-")
The cow visits the cat.
Unknown
random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "+")
The cow does not chase the tiger.
Unknown
inv-random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat visits the cow.[(triple1)] The cow chases the lion.[(triple2)] The lion chases the cow.[(triple3)] The tiger eats the cow.[(triple4)] @1: The tiger is cold.[(((triple4) -> rule1))] @2: The tiger chases the lion.[(((((triple4) -> rule1)) -> rule3))]
The cat visits the cow.
("cat" "visits" "cow" "+")
triple1
The cow chases the lion.
("cow" "chases" "lion" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2