The dog is big. The dog is blue. The dog is kind. All kind, blue things are big. All kind things are young. If something is blue and kind then it is young. If the dog is kind and the dog is not big then the dog is young. If something is big and not blue then it is not red. If something is young then it is red.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
All kind, blue things are big.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is blue and kind then it is young.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If the dog is kind and the dog is not big then the dog is young.
((("dog" "is" "kind" "+") ("dog" "is" "big" "~")) -> ("dog" "is" "young" "+"))
If something is big and not blue then it is not red.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "red" "-"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
The dog is kind.
True
1
proof
[(triple3)]
("dog" "is" "kind" "+")
triple3
The dog is not blue.
False
1
inv-proof
[(triple2)]
("dog" "is" "blue" "-")
triple2
The dog is young.
True
2
proof
[(((triple3) -> rule2) OR ((triple2 triple3) -> rule3))]
("dog" "is" "young" "+")
((triple3) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((triple2 triple3) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple2 triple3) -> rule3))]
("dog" "is" "young" "-")
((triple3) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((triple2 triple3) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
True
3
proof
[(((((triple3) -> rule2)) -> rule6) OR ((((triple2 triple3) -> rule3)) -> rule6))]
("dog" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((((triple2 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not red.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6) OR ((((triple2 triple3) -> rule3)) -> rule6))]
("dog" "is" "red" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((((triple2 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is big.[(triple1 OR ((triple3 triple2) -> rule1))] The dog is blue.[(triple2)] The dog is kind.[(triple3)] @1: The dog is young.[(((triple3) -> rule2) OR ((triple2 triple3) -> rule3))] @2: The dog is red.[(((((triple3) -> rule2)) -> rule6) OR ((((triple2 triple3) -> rule3)) -> rule6))]
The dog is big.
("dog" "is" "big" "+")
triple1
((triple3 triple2) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
((triple3) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((triple2 triple3) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((((triple2 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2