The cow chases the dog. The cow is kind. The cow is rough. The cow sees the lion. The dog is cold. The dog sees the lion. The lion does not chase the squirrel. The lion is not big. The lion sees the dog. The squirrel likes the dog. The squirrel likes the lion. If the squirrel likes the lion then the squirrel sees the cow. If something sees the dog then the dog is rough. If something sees the cow and it likes the lion then it is big. If something is cold then it chases the dog. Kind things are cold. If something chases the cow then it does not see the cow. All big things are kind. If something is green and not big then it likes the cow. If the cow is not kind then the cow likes the squirrel.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
The lion is not big.
("lion" "is" "big" "-")
The lion sees the dog.
("lion" "sees" "dog" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If the squirrel likes the lion then the squirrel sees the cow.
((("squirrel" "likes" "lion" "+")) -> ("squirrel" "sees" "cow" "+"))
If something sees the dog then the dog is rough.
((("something" "sees" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something sees the cow and it likes the lion then it is big.
((("something" "sees" "cow" "+") ("something" "likes" "lion" "+")) -> ("something" "is" "big" "+"))
If something is cold then it chases the dog.
((("something" "is" "cold" "+")) -> ("something" "chases" "dog" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something chases the cow then it does not see the cow.
((("something" "chases" "cow" "+")) -> ("something" "sees" "cow" "-"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is green and not big then it likes the cow.
((("something" "is" "green" "+") ("something" "is" "big" "~")) -> ("something" "likes" "cow" "+"))
If the cow is not kind then the cow likes the squirrel.
((("cow" "is" "kind" "~")) -> ("cow" "likes" "squirrel" "+"))
The lion does not chase the squirrel.
True
1
proof
[(triple7)]
("lion" "chases" "squirrel" "-")
triple7
The lion chases the squirrel.
False
1
inv-proof
[(triple7)]
("lion" "chases" "squirrel" "+")
triple7
The dog is rough.
True
2
proof
[(((triple9) -> rule2))]
("dog" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is not rough.
False
2
inv-proof
[(((triple9) -> rule2))]
("dog" "is" "rough" "-")
((triple9) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The squirrel is big.
True
4
proof
[(((((triple11) -> rule1) triple11) -> rule3))]
("squirrel" "is" "big" "+")
((((triple11) -> (rule1 % int2)) triple11) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel is not big.
False
4
inv-proof
[(((((triple11) -> rule1) triple11) -> rule3))]
("squirrel" "is" "big" "-")
((((triple11) -> (rule1 % int2)) triple11) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel is kind.
True
5
proof
[(((((((triple11) -> rule1) triple11) -> rule3)) -> rule7))]
("squirrel" "is" "kind" "+")
((((((triple11) -> (rule1 % int3)) triple11) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int3
The squirrel is not kind.
False
5
inv-proof
[(((((((triple11) -> rule1) triple11) -> rule3)) -> rule7))]
("squirrel" "is" "kind" "-")
((((((triple11) -> (rule1 % int3)) triple11) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int3
The squirrel is cold.
True
6
proof
[(((((((((triple11) -> rule1) triple11) -> rule3)) -> rule7)) -> rule5))]
("squirrel" "is" "cold" "+")
((((((((triple11) -> (rule1 % int4)) triple11) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int4
The squirrel is not cold.
False
6
inv-proof
[(((((((((triple11) -> rule1) triple11) -> rule3)) -> rule7)) -> rule5))]
("squirrel" "is" "cold" "-")
((((((((triple11) -> (rule1 % int4)) triple11) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int4
The squirrel chases the dog.
True
7
proof
[(((((((((((triple11) -> rule1) triple11) -> rule3)) -> rule7)) -> rule5)) -> rule4))]
("squirrel" "chases" "dog" "+")
((((((((((triple11) -> (rule1 % int5)) triple11) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int5
The squirrel does not chase the dog.
False
7
inv-proof
[(((((((((((triple11) -> rule1) triple11) -> rule3)) -> rule7)) -> rule5)) -> rule4))]
("squirrel" "chases" "dog" "-")
((((((((((triple11) -> (rule1 % int5)) triple11) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int5
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "kind" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "likes" "cow" "+")
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "big" "-")
The lion chases the dog.
Unknown
rconc
[@3: The lion chases the dog.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule7 <- FAIL)]]
("lion" "chases" "dog" "+")
The lion is not cold.
Unknown
inv-rconc
[@2: The lion is cold.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("lion" "is" "cold" "-")
The dog likes the cow.
Unknown
rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "likes" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The lion chases the cow.
Unknown
random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The cow chases the dog.[(triple1 OR ((((triple2) -> rule5)) -> rule4))] The cow is kind.[(triple2)] The cow is rough.[(triple3)] The cow sees the lion.[(triple4)] The dog is cold.[(triple5)] The dog sees the lion.[(triple6)] The lion does not chase the squirrel.[(triple7)] The lion is not big.[(triple8)] The lion sees the dog.[(triple9)] The squirrel likes the dog.[(triple10)] The squirrel likes the lion.[(triple11)] @1: The cow is cold.[(((triple2) -> rule5))] The dog chases the dog.[(((triple5) -> rule4))] The dog is rough.[(((triple9) -> rule2))] The squirrel sees the cow.[(((triple11) -> rule1))] @2: The squirrel is big.[(((((triple11) -> rule1) triple11) -> rule3))] @3: The squirrel is kind.[(((((((triple11) -> rule1) triple11) -> rule3)) -> rule7))] @4: The squirrel is cold.[(((((((((triple11) -> rule1) triple11) -> rule3)) -> rule7)) -> rule5))] @5: The squirrel chases the dog.[(((((((((((triple11) -> rule1) triple11) -> rule3)) -> rule7)) -> rule5)) -> rule4))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog sees the lion.
("dog" "sees" "lion" "+")
triple6
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
triple7
The lion is not big.
("lion" "is" "big" "-")
triple8
The lion sees the dog.
("lion" "sees" "dog" "+")
triple9
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple10
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple11
The cow is cold.
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple5) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((triple9) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple11) -> (rule1 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple11) -> (rule1 % int2)) triple11) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((((triple11) -> (rule1 % int3)) triple11) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((((triple11) -> (rule1 % int4)) triple11) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int4
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
((((((((((triple11) -> (rule1 % int5)) triple11) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel is big.
("squirrel" "is" "big" "+")
int4
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int5