The cow chases the lion. The cow is kind. The lion likes the cow. If something is red then it is young. If the cow is red and the cow is blue then the cow likes the lion. If the lion chases the cow then the cow chases the lion. If something chases the lion and it is kind then it is red. If the cow needs the lion then the cow chases the lion. If something is young and kind then it chases the cow.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is kind.
("cow" "is" "kind" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If the cow is red and the cow is blue then the cow likes the lion.
((("cow" "is" "red" "+") ("cow" "is" "blue" "+")) -> ("cow" "likes" "lion" "+"))
If the lion chases the cow then the cow chases the lion.
((("lion" "chases" "cow" "+")) -> ("cow" "chases" "lion" "+"))
If something chases the lion and it is kind then it is red.
((("something" "chases" "lion" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If the cow needs the lion then the cow chases the lion.
((("cow" "needs" "lion" "+")) -> ("cow" "chases" "lion" "+"))
If something is young and kind then it chases the cow.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "chases" "cow" "+"))
The cow is kind.
True
1
proof
[(triple2)]
("cow" "is" "kind" "+")
triple2
The cow is not kind.
False
1
inv-proof
[(triple2)]
("cow" "is" "kind" "-")
triple2
The cow is red.
True
3
proof
[(((triple1 triple2) -> rule4))]
("cow" "is" "red" "+")
((triple1 triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
3
inv-proof
[(((triple1 triple2) -> rule4))]
("cow" "is" "red" "-")
((triple1 triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is young.
True
4
proof
[(((((triple1 triple2) -> rule4)) -> rule1))]
("cow" "is" "young" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is not young.
False
4
inv-proof
[(((((triple1 triple2) -> rule4)) -> rule1))]
("cow" "is" "young" "-")
((((triple1 triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow chases the cow.
True
6
proof
[(((((((triple1 triple2) -> rule4)) -> rule1) triple2) -> rule6))]
("cow" "chases" "cow" "+")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow does not chase the cow.
False
6
inv-proof
[(((((((triple1 triple2) -> rule4)) -> rule1) triple2) -> rule6))]
("cow" "chases" "cow" "-")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow does not like the lion.
Unknown
inv-rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "lion" "-")
The lion is young.
Unknown
rconc
[@2: The lion is young.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("lion" "is" "young" "+")
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "red" "-")
The lion chases the cow.
Unknown
rconc
[@1: The lion chases the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "cow" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The cow chases the lion.[(triple1)] The cow is kind.[(triple2)] The lion likes the cow.[(triple3)] @1: The cow is red.[(((triple1 triple2) -> rule4))] @2: The cow is young.[(((((triple1 triple2) -> rule4)) -> rule1))] @3: The cow chases the cow.[(((((((triple1 triple2) -> rule4)) -> rule1) triple2) -> rule6))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The lion likes the cow.
("lion" "likes" "cow" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
((triple1 triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple1 triple2) -> (rule4 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3