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