The dog is blue. The dog is rough. The dog is young. If the dog is rough then the dog is big. All rough, blue people are young. If someone is blue and rough then they are not red. If the dog is red and the dog is big then the dog is blue. Big people are blue. If someone is red and not big then they are not blue. If the dog is big then the dog is young. If the dog is not big and the dog is not blue then the dog is young.
The dog is blue.
("dog" "is" "blue" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
If the dog is rough then the dog is big.
((("dog" "is" "rough" "+")) -> ("dog" "is" "big" "+"))
All rough, blue people are young.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and rough then they are not red.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
If the dog is red and the dog is big then the dog is blue.
((("dog" "is" "red" "+") ("dog" "is" "big" "+")) -> ("dog" "is" "blue" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and not big then they are not blue.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "blue" "-"))
If the dog is big then the dog is young.
((("dog" "is" "big" "+")) -> ("dog" "is" "young" "+"))
If the dog is not big and the dog is not blue then the dog is young.
((("dog" "is" "big" "~") ("dog" "is" "blue" "~")) -> ("dog" "is" "young" "+"))
The dog is young.
True
1
proof
[(triple3 OR ((triple2 triple1) -> rule2) OR ((((triple2) -> rule1)) -> rule7) OR ((triple2 ((((triple2) -> rule1)) -> rule5)) -> rule2))]
("dog" "is" "young" "+")
triple3
((triple2 triple1) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is not rough.
False
1
inv-proof
[(triple2)]
("dog" "is" "rough" "-")
triple2
The dog is not red.
True
3
proof
[(((triple1 triple2) -> rule3) OR ((((((triple2) -> rule1)) -> rule5) triple2) -> rule3))]
("dog" "is" "red" "-")
((triple1 triple2) -> (rule3 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "is" "big" "-")
((triple2) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
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 dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is blue.[(triple1 OR ((((triple2) -> rule1)) -> rule5))] The dog is rough.[(triple2)] The dog is young.[(triple3 OR ((triple2 triple1) -> rule2) OR ((((triple2) -> rule1)) -> rule7) OR ((triple2 ((((triple2) -> rule1)) -> rule5)) -> rule2))] @1: The dog is big.[(((triple2) -> rule1))] The dog is not red.[(((triple1 triple2) -> rule3) OR ((((((triple2) -> rule1)) -> rule5) triple2) -> rule3))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
((triple2 triple1) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is big.
("dog" "is" "big" "+")
((triple2) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is not red.
("dog" "is" "red" "-")
((triple1 triple2) -> (rule3 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3