The dog is big. The dog is blue. The dog is kind. The dog is round. The dog is young. All young, big things are kind. All young things are round. If something is kind and big then it is blue. All young, blue things are kind. If the dog is kind then the dog is young. If the dog is big then the dog is kind.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
All young, big things are kind.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is kind and big then it is blue.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All young, blue things are kind.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If the dog is kind then the dog is young.
((("dog" "is" "kind" "+")) -> ("dog" "is" "young" "+"))
If the dog is big then the dog is kind.
((("dog" "is" "big" "+")) -> ("dog" "is" "kind" "+"))
The dog is blue.
True
1
proof
[(triple2 OR ((triple3 triple1) -> rule3) OR ((((triple1) -> rule6) triple1) -> rule3) OR ((((triple5 triple1) -> rule1) triple1) -> rule3))]
("dog" "is" "blue" "+")
triple2
((triple3 triple1) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
((((triple5 triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is not round.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule2) OR ((((triple3) -> rule5)) -> rule2) OR ((((((triple1) -> rule6)) -> rule5)) -> rule2))]
("dog" "is" "round" "-")
triple4
((triple5) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog is big.[(triple1)] The dog is blue.[(triple2 OR ((triple3 triple1) -> rule3) OR ((((triple1) -> rule6) triple1) -> rule3) OR ((((triple5 triple1) -> rule1) triple1) -> rule3))] The dog is kind.[(triple3 OR ((triple1) -> rule6) OR ((triple5 triple1) -> rule1) OR ((triple5 triple2) -> rule4))] The dog is round.[(triple4 OR ((triple5) -> rule2) OR ((((triple3) -> rule5)) -> rule2) OR ((((((triple1) -> rule6)) -> rule5)) -> rule2))] The dog is young.[(triple5 OR ((triple3) -> rule5) OR ((((triple1) -> rule6)) -> rule5))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
((triple3 triple1) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
((((triple5 triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
triple3
((triple1) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((triple5 triple1) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((triple5 triple2) -> (rule4 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is round.
("dog" "is" "round" "+")
triple4
((triple5) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog is young.
("dog" "is" "young" "+")
triple5
((triple3) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2