The cat is cold. The cat is young. The cat sees the dog. The cat visits the dog. The dog is big. The dog is kind. The dog is young. The dog needs the cat. The dog sees the cat. The dog visits the cat. If something is young then it is blue. If something visits the cat then it visits the dog. If something sees the cat and the cat needs the dog then the cat visits the dog. If something sees the dog then it sees the cat. If the dog visits the cat and the dog needs the cat then the cat is big. If something visits the dog and the dog visits the cat then the dog is kind. If something needs the dog then the dog sees the cat. If something is blue then it sees the dog.
The cat is cold.
("cat" "is" "cold" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something visits the cat then it visits the dog.
((("something" "visits" "cat" "+")) -> ("something" "visits" "dog" "+"))
If something sees the cat and the cat needs the dog then the cat visits the dog.
((("something" "sees" "cat" "+") ("cat" "needs" "dog" "+")) -> ("cat" "visits" "dog" "+"))
If something sees the dog then it sees the cat.
((("something" "sees" "dog" "+")) -> ("something" "sees" "cat" "+"))
If the dog visits the cat and the dog needs the cat then the cat is big.
((("dog" "visits" "cat" "+") ("dog" "needs" "cat" "+")) -> ("cat" "is" "big" "+"))
If something visits the dog and the dog visits the cat then the dog is kind.
((("something" "visits" "dog" "+") ("dog" "visits" "cat" "+")) -> ("dog" "is" "kind" "+"))
If something needs the dog then the dog sees the cat.
((("something" "needs" "dog" "+")) -> ("dog" "sees" "cat" "+"))
If something is blue then it sees the dog.
((("something" "is" "blue" "+")) -> ("something" "sees" "dog" "+"))
The cat visits the dog.
True
1
proof
[(triple4)]
("cat" "visits" "dog" "+")
triple4
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The cat is big.
True
3
proof
[(((triple10 triple8) -> rule5))]
("cat" "is" "big" "+")
((triple10 triple8) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "is" "blue" "-")
((triple2) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The dog sees the dog.
True
3
proof
[(((((triple7) -> rule1)) -> rule8))]
("dog" "sees" "dog" "+")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not see the dog.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule8))]
("dog" "sees" "dog" "-")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The cat needs the dog.
Unknown
random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
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 young.[(triple2)] The cat sees the dog.[(triple3 OR ((((triple2) -> rule1)) -> rule8))] The cat visits the dog.[(triple4)] The dog is big.[(triple5)] The dog is kind.[(triple6 OR ((triple4 triple10) -> rule6) OR ((((triple10) -> rule2) triple10) -> rule6))] The dog is young.[(triple7)] The dog needs the cat.[(triple8)] The dog sees the cat.[(triple9 OR ((((((triple7) -> rule1)) -> rule8)) -> rule4))] The dog visits the cat.[(triple10)] @1: The cat is big.[(((triple10 triple8) -> rule5))] The cat is blue.[(((triple2) -> rule1))] The cat sees the cat.[(((triple3) -> rule4) OR ((((((triple2) -> rule1)) -> rule8)) -> rule4))] The dog is blue.[(((triple7) -> rule1))] The dog visits the dog.[(((triple10) -> rule2))] @2: The dog sees the dog.[(((((triple7) -> rule1)) -> rule8))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog is kind.
("dog" "is" "kind" "+")
triple6
((triple4 triple10) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((((triple10) -> (rule2 % int2)) triple10) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is young.
("dog" "is" "young" "+")
triple7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple8
The dog sees the cat.
("dog" "sees" "cat" "+")
triple9
((((((triple7) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
triple10
The cat is big.
("cat" "is" "big" "+")
((triple10 triple8) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple3) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
((triple7) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple10) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2