The cow chases the dog. The cow is big. The cow is rough. The cow sees the dog. The dog is big. The dog is red. The dog needs the cow. The dog sees the cow. The dog sees the lion. The lion chases the cow. The lion chases the dog. The lion is big. The lion is blue. The lion is red. The lion sees the dog. If something needs the lion then the lion is rough. If something chases the dog and it sees the cow then the dog is rough. If something chases the cow then it is blue. If something sees the cow then it chases the cow. Red things are kind. If something sees the lion and it needs the lion then the lion sees the cow. If the dog sees the lion then the lion is kind. If something is red and kind then it needs the lion.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If something needs the lion then the lion is rough.
((("something" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
If something chases the dog and it sees the cow then the dog is rough.
((("something" "chases" "dog" "+") ("something" "sees" "cow" "+")) -> ("dog" "is" "rough" "+"))
If something chases the cow then it is blue.
((("something" "chases" "cow" "+")) -> ("something" "is" "blue" "+"))
If something sees the cow then it chases the cow.
((("something" "sees" "cow" "+")) -> ("something" "chases" "cow" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something sees the lion and it needs the lion then the lion sees the cow.
((("something" "sees" "lion" "+") ("something" "needs" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If the dog sees the lion then the lion is kind.
((("dog" "sees" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something is red and kind then it needs the lion.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "lion" "+"))
The dog is red.
True
1
proof
[(triple6)]
("dog" "is" "red" "+")
triple6
The cow does not chase the dog.
False
1
inv-proof
[(triple1)]
("cow" "chases" "dog" "-")
triple1
The dog is kind.
True
2
proof
[(((triple6) -> rule5))]
("dog" "is" "kind" "+")
((triple6) -> (rule5 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple14) -> rule5) OR ((triple9) -> rule7))]
("lion" "is" "kind" "-")
((triple14) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple9) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion needs the lion.
True
4
proof
[(((triple14 ((triple14) -> rule5)) -> rule8) OR ((triple14 ((triple9) -> rule7)) -> rule8))]
("lion" "needs" "lion" "+")
((triple14 ((triple14) -> (rule5 % int2))) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple14 ((triple9) -> (rule7 % int2))) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The dog is not blue.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule3))]
("dog" "is" "blue" "-")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The lion is rough.
True
5
proof
[(((((triple14 ((triple14) -> rule5)) -> rule8)) -> rule1) OR ((((triple14 ((triple9) -> rule7)) -> rule8)) -> rule1) OR ((((triple6 ((triple6) -> rule5)) -> rule8)) -> rule1))]
("lion" "is" "rough" "+")
((((triple14 ((triple14) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple14 ((triple9) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The lion is not rough.
False
5
inv-proof
[(((((triple14 ((triple14) -> rule5)) -> rule8)) -> rule1) OR ((((triple14 ((triple9) -> rule7)) -> rule8)) -> rule1) OR ((((triple6 ((triple6) -> rule5)) -> rule8)) -> rule1))]
("lion" "is" "rough" "-")
((((triple14 ((triple14) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple14 ((triple9) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "kind" "-")
The cow is blue.
Unknown
rconc
[@2: The cow is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("cow" "is" "blue" "+")
The cow does not need the lion.
Unknown
inv-rconc
[@1: The cow needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "needs" "lion" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cow" "+")
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 cow needs the dog.
Unknown
random
[@0: The cow needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "dog" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The dog chases the lion.
Unknown
random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "+")
@0: The cow chases the dog.[(triple1)] The cow is big.[(triple2)] The cow is rough.[(triple3)] The cow sees the dog.[(triple4)] The dog is big.[(triple5)] The dog is red.[(triple6)] The dog needs the cow.[(triple7)] The dog sees the cow.[(triple8)] The dog sees the lion.[(triple9)] The lion chases the cow.[(triple10 OR ((((triple9 ((triple6 ((triple6) -> rule5)) -> rule8)) -> rule6)) -> rule4))] The lion chases the dog.[(triple11)] The lion is big.[(triple12)] The lion is blue.[(triple13 OR ((triple10) -> rule3) OR ((((((triple9 ((triple6 ((triple6) -> rule5)) -> rule8)) -> rule6)) -> rule4)) -> rule3))] The lion is red.[(triple14)] The lion sees the dog.[(triple15)] @1: The dog chases the cow.[(((triple8) -> rule4))] The dog is kind.[(((triple6) -> rule5))] The lion is kind.[(((triple14) -> rule5) OR ((triple9) -> rule7))] @2: The dog is blue.[(((((triple8) -> rule4)) -> rule3))] The dog needs the lion.[(((triple6 ((triple6) -> rule5)) -> rule8))] The lion needs the lion.[(((triple14 ((triple14) -> rule5)) -> rule8) OR ((triple14 ((triple9) -> rule7)) -> rule8))] @3: The lion is rough.[(((((triple14 ((triple14) -> rule5)) -> rule8)) -> rule1) OR ((((triple14 ((triple9) -> rule7)) -> rule8)) -> rule1) OR ((((triple6 ((triple6) -> rule5)) -> rule8)) -> rule1))] The lion sees the cow.[(((triple9 ((triple6 ((triple6) -> rule5)) -> rule8)) -> rule6))] @4: The dog is rough.[(((triple11 ((triple9 ((triple6 ((triple6) -> rule5)) -> rule8)) -> rule6)) -> rule2))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog needs the cow.
("dog" "needs" "cow" "+")
triple7
The dog sees the cow.
("dog" "sees" "cow" "+")
triple8
The dog sees the lion.
("dog" "sees" "lion" "+")
triple9
The lion chases the cow.
("lion" "chases" "cow" "+")
triple10
((((triple9 ((triple6 ((triple6) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple11
The lion is big.
("lion" "is" "big" "+")
triple12
The lion is blue.
("lion" "is" "blue" "+")
triple13
((triple10) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((((triple9 ((triple6 ((triple6) -> (rule5 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
int5
The lion is red.
("lion" "is" "red" "+")
triple14
The lion sees the dog.
("lion" "sees" "dog" "+")
triple15
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple8) -> (rule4 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple6) -> (rule5 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple14) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple9) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule8 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple14 ((triple14) -> (rule5 % int2))) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple14 ((triple9) -> (rule7 % int2))) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((triple14 ((triple14) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple14 ((triple9) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple9 ((triple6 ((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
((triple11 ((triple9 ((triple6 ((triple6) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4