The cat is red. The cow chases the cat. The cow chases the tiger. The cow sees the lion. The lion chases the cat. The lion chases the cow. The tiger chases the cow. If something is green then it is young. If something sees the cow then the cow is cold. If something sees the lion then the lion needs the cat. If something chases the cow and the cow is green then it sees the lion. If something chases the cow and it needs the lion then it chases the tiger. If the tiger chases the cow then the cow needs the tiger. If something needs the cat then the cat sees the cow. If the tiger is red and the tiger is cold then the tiger sees the cat.
The cat is red.
("cat" "is" "red" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something sees the cow then the cow is cold.
((("something" "sees" "cow" "+")) -> ("cow" "is" "cold" "+"))
If something sees the lion then the lion needs the cat.
((("something" "sees" "lion" "+")) -> ("lion" "needs" "cat" "+"))
If something chases the cow and the cow is green then it sees the lion.
((("something" "chases" "cow" "+") ("cow" "is" "green" "+")) -> ("something" "sees" "lion" "+"))
If something chases the cow and it needs the lion then it chases the tiger.
((("something" "chases" "cow" "+") ("something" "needs" "lion" "+")) -> ("something" "chases" "tiger" "+"))
If the tiger chases the cow then the cow needs the tiger.
((("tiger" "chases" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
If something needs the cat then the cat sees the cow.
((("something" "needs" "cat" "+")) -> ("cat" "sees" "cow" "+"))
If the tiger is red and the tiger is cold then the tiger sees the cat.
((("tiger" "is" "red" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "sees" "cat" "+"))
The cat is red.
True
1
proof
[(triple1)]
("cat" "is" "red" "+")
triple1
The tiger does not chase the cow.
False
1
inv-proof
[(triple7)]
("tiger" "chases" "cow" "-")
triple7
The cow needs the tiger.
True
2
proof
[(((triple7) -> rule6))]
("cow" "needs" "tiger" "+")
((triple7) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The lion does not need the cat.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "needs" "cat" "-")
((triple4) -> (rule3 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat sees the cow.
True
3
proof
[(((((triple4) -> rule3)) -> rule7))]
("cat" "sees" "cow" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat does not see the cow.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule7))]
("cat" "sees" "cow" "-")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cow is cold.
True
4
proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule2))]
("cow" "is" "cold" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The cow is not cold.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule2))]
("cow" "is" "cold" "-")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "young" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "young" "+")
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "young" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "lion" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
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 cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cat is red.[(triple1)] The cow chases the cat.[(triple2)] The cow chases the tiger.[(triple3)] The cow sees the lion.[(triple4)] The lion chases the cat.[(triple5)] The lion chases the cow.[(triple6)] The tiger chases the cow.[(triple7)] @1: The cow needs the tiger.[(((triple7) -> rule6))] The lion needs the cat.[(((triple4) -> rule3))] @2: The cat sees the cow.[(((((triple4) -> rule3)) -> rule7))] @3: The cow is cold.[(((((((triple4) -> rule3)) -> rule7)) -> rule2))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The lion chases the cat.
("lion" "chases" "cat" "+")
triple5
The lion chases the cow.
("lion" "chases" "cow" "+")
triple6
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple7
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple7) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
((triple4) -> (rule3 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3