The cat is cold. The cat is nice. The cat is young. The cat needs the cow. The cow eats the cat. The cow eats the lion. The cow is kind. The cow is nice. The cow is young. The cow needs the cat. The cow needs the lion. The cow sees the lion. The lion eats the cat. The lion is kind. The lion is young. The lion sees the cat. If someone needs the cat and they are kind then they are round. If the lion needs the cat and the lion needs the cow then the lion sees the cat. If someone sees the cow then the cow sees the cat. If someone needs the cow and the cow is cold then they are young. If the cat sees the lion and the lion is round then the cat eats the cow. If someone needs the cat then they are cold. If someone sees the cat then they see the cow. If the lion sees the cow then the cow sees the cat.
The cat is cold.
("cat" "is" "cold" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If someone needs the cat and they are kind then they are round.
((("someone" "needs" "cat" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If the lion needs the cat and the lion needs the cow then the lion sees the cat.
((("lion" "needs" "cat" "+") ("lion" "needs" "cow" "+")) -> ("lion" "sees" "cat" "+"))
If someone sees the cow then the cow sees the cat.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "cat" "+"))
If someone needs the cow and the cow is cold then they are young.
((("someone" "needs" "cow" "+") ("cow" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If the cat sees the lion and the lion is round then the cat eats the cow.
((("cat" "sees" "lion" "+") ("lion" "is" "round" "+")) -> ("cat" "eats" "cow" "+"))
If someone needs the cat then they are cold.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cat then they see the cow.
((("someone" "sees" "cat" "+")) -> ("someone" "sees" "cow" "+"))
If the lion sees the cow then the cow sees the cat.
((("lion" "sees" "cow" "+")) -> ("cow" "sees" "cat" "+"))
The lion is young.
True
1
proof
[(triple15)]
("lion" "is" "young" "+")
triple15
The cow is not kind.
False
1
inv-proof
[(triple7)]
("cow" "is" "kind" "-")
triple7
The lion sees the cow.
True
2
proof
[(((triple16) -> rule7))]
("lion" "sees" "cow" "+")
((triple16) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple10) -> rule6))]
("cow" "is" "cold" "-")
((triple10) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the cat.
True
3
proof
[(((((triple16) -> rule7)) -> rule3) OR ((((triple16) -> rule7)) -> rule8))]
("cow" "sees" "cat" "+")
((((triple16) -> (rule7 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
((((triple16) -> (rule7 % int2))) -> (rule8 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow does not see the cat.
False
3
inv-proof
[(((((triple16) -> rule7)) -> rule3) OR ((((triple16) -> rule7)) -> rule8))]
("cow" "sees" "cat" "-")
((((triple16) -> (rule7 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
((((triple16) -> (rule7 % int2))) -> (rule8 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow sees the cow.
True
4
proof
[(((((((triple16) -> rule7)) -> rule3)) -> rule7) OR ((((((triple16) -> rule7)) -> rule8)) -> rule7))]
("cow" "sees" "cow" "+")
((((((triple16) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
((((((triple16) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The cow does not see the cow.
False
4
inv-proof
[(((((((triple16) -> rule7)) -> rule3)) -> rule7) OR ((((((triple16) -> rule7)) -> rule8)) -> rule7))]
("cow" "sees" "cow" "-")
((((((triple16) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
((((((triple16) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "round" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "round" "+")
The cat does not eat the cow.
Unknown
inv-rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "cow" "-")
The cat sees the cow.
Unknown
rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "sees" "cow" "+")
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat is cold.[(triple1)] The cat is nice.[(triple2)] The cat is young.[(triple3 OR ((triple4 ((triple10) -> rule6)) -> rule4))] The cat needs the cow.[(triple4)] The cow eats the cat.[(triple5)] The cow eats the lion.[(triple6)] The cow is kind.[(triple7)] The cow is nice.[(triple8)] The cow is young.[(triple9)] The cow needs the cat.[(triple10)] The cow needs the lion.[(triple11)] The cow sees the lion.[(triple12)] The lion eats the cat.[(triple13)] The lion is kind.[(triple14)] The lion is young.[(triple15)] The lion sees the cat.[(triple16)] @1: The cow is cold.[(((triple10) -> rule6))] The cow is round.[(((triple10 triple7) -> rule1))] The lion sees the cow.[(((triple16) -> rule7))] @2: The cow sees the cat.[(((((triple16) -> rule7)) -> rule3) OR ((((triple16) -> rule7)) -> rule8))] @3: The cow sees the cow.[(((((((triple16) -> rule7)) -> rule3)) -> rule7) OR ((((((triple16) -> rule7)) -> rule8)) -> rule7))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
((triple4 ((triple10) -> (rule6 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple5
The cow eats the lion.
("cow" "eats" "lion" "+")
triple6
The cow is kind.
("cow" "is" "kind" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
triple8
The cow is young.
("cow" "is" "young" "+")
triple9
The cow needs the cat.
("cow" "needs" "cat" "+")
triple10
The cow needs the lion.
("cow" "needs" "lion" "+")
triple11
The cow sees the lion.
("cow" "sees" "lion" "+")
triple12
The lion eats the cat.
("lion" "eats" "cat" "+")
triple13
The lion is kind.
("lion" "is" "kind" "+")
triple14
The lion is young.
("lion" "is" "young" "+")
triple15
The lion sees the cat.
("lion" "sees" "cat" "+")
triple16
The cow is cold.
("cow" "is" "cold" "+")
((triple10) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((triple10 triple7) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple16) -> (rule7 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
((((triple16) -> (rule7 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
((((triple16) -> (rule7 % int2))) -> (rule8 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((triple16) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
((((((triple16) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3