The cat chases the dog. The cat is big. The cat is blue. The cat is kind. The cat is rough. The dog chases the cat. The dog is blue. The dog is round. The dog sees the cat. The dog visits the cat. If someone is big then they visit the dog. If the dog is big then the dog is blue. If someone sees the dog then they chase the cat. If someone sees the dog and they see the cat then the cat is kind. If someone is kind then they visit the dog. If someone visits the cat and the cat visits the dog then the cat sees the dog. If the dog chases the cat then the cat is big. If the cat visits the dog and the dog is blue then the dog sees the cat.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If someone is big then they visit the dog.
((("someone" "is" "big" "+")) -> ("someone" "visits" "dog" "+"))
If the dog is big then the dog is blue.
((("dog" "is" "big" "+")) -> ("dog" "is" "blue" "+"))
If someone sees the dog then they chase the cat.
((("someone" "sees" "dog" "+")) -> ("someone" "chases" "cat" "+"))
If someone sees the dog and they see the cat then the cat is kind.
((("someone" "sees" "dog" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone is kind then they visit the dog.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the cat and the cat visits the dog then the cat sees the dog.
((("someone" "visits" "cat" "+") ("cat" "visits" "dog" "+")) -> ("cat" "sees" "dog" "+"))
If the dog chases the cat then the cat is big.
((("dog" "chases" "cat" "+")) -> ("cat" "is" "big" "+"))
If the cat visits the dog and the dog is blue then the dog sees the cat.
((("cat" "visits" "dog" "+") ("dog" "is" "blue" "+")) -> ("dog" "sees" "cat" "+"))
The dog is blue.
True
1
proof
[(triple7)]
("dog" "is" "blue" "+")
triple7
The dog is not round.
False
1
inv-proof
[(triple8)]
("dog" "is" "round" "-")
triple8
The cat visits the dog.
True
2
proof
[(((triple2) -> rule1) OR ((triple4) -> rule5) OR ((((triple6) -> rule7)) -> rule1))]
("cat" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
((triple4) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple4) -> rule5) OR ((((triple6) -> rule7)) -> rule1))]
("cat" "visits" "dog" "-")
((triple2) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
((triple4) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat sees the dog.
True
4
proof
[(((triple10 ((triple2) -> rule1)) -> rule6) OR ((triple10 ((triple4) -> rule5)) -> rule6) OR ((triple10 ((((triple6) -> rule7)) -> rule1)) -> rule6))]
("cat" "sees" "dog" "+")
((triple10 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((triple10 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((triple10 ((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The cat does not see the dog.
False
4
inv-proof
[(((triple10 ((triple2) -> rule1)) -> rule6) OR ((triple10 ((triple4) -> rule5)) -> rule6) OR ((triple10 ((((triple6) -> rule7)) -> rule1)) -> rule6))]
("cat" "sees" "dog" "-")
((triple10 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((triple10 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((triple10 ((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The cat chases the cat.
True
5
proof
[(((((triple10 ((triple2) -> rule1)) -> rule6)) -> rule3) OR ((((triple10 ((triple4) -> rule5)) -> rule6)) -> rule3) OR ((((triple10 ((((triple6) -> rule7)) -> rule1)) -> rule6)) -> rule3))]
("cat" "chases" "cat" "+")
((((triple10 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((triple10 ((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((triple10 ((((triple6) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The cat does not chase the cat.
False
5
inv-proof
[(((((triple10 ((triple2) -> rule1)) -> rule6)) -> rule3) OR ((((triple10 ((triple4) -> rule5)) -> rule6)) -> rule3) OR ((((triple10 ((((triple6) -> rule7)) -> rule1)) -> rule6)) -> rule3))]
("cat" "chases" "cat" "-")
((((triple10 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((triple10 ((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((triple10 ((((triple6) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "dog" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cat chases the dog.[(triple1)] The cat is big.[(triple2 OR ((triple6) -> rule7))] The cat is blue.[(triple3)] The cat is kind.[(triple4)] The cat is rough.[(triple5)] The dog chases the cat.[(triple6)] The dog is blue.[(triple7)] The dog is round.[(triple8)] The dog sees the cat.[(triple9 OR ((((triple2) -> rule1) triple7) -> rule8) OR ((((triple4) -> rule5) triple7) -> rule8) OR ((((((triple6) -> rule7)) -> rule1) triple7) -> rule8))] The dog visits the cat.[(triple10)] @1: The cat visits the dog.[(((triple2) -> rule1) OR ((triple4) -> rule5) OR ((((triple6) -> rule7)) -> rule1))] @2: The cat sees the dog.[(((triple10 ((triple2) -> rule1)) -> rule6) OR ((triple10 ((triple4) -> rule5)) -> rule6) OR ((triple10 ((((triple6) -> rule7)) -> rule1)) -> rule6))] @3: The cat chases the cat.[(((((triple10 ((triple2) -> rule1)) -> rule6)) -> rule3) OR ((((triple10 ((triple4) -> rule5)) -> rule6)) -> rule3) OR ((((triple10 ((((triple6) -> rule7)) -> rule1)) -> rule6)) -> rule3))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
((triple6) -> (rule7 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The dog chases the cat.
("dog" "chases" "cat" "+")
triple6
The dog is blue.
("dog" "is" "blue" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
triple8
The dog sees the cat.
("dog" "sees" "cat" "+")
triple9
((((triple2) -> (rule1 % int2)) triple7) -> (rule8 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((((triple4) -> (rule5 % int2)) triple7) -> (rule8 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((((((triple6) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule8 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
triple10
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
((triple4) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat sees the dog.
("cat" "sees" "dog" "+")
((triple10 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((triple10 ((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
((triple10 ((((triple6) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple10 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((triple10 ((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((triple10 ((((triple6) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4