The dog is red. If something is blue and rough then it is nice. If the dog is red then the dog is rough. Red, rough things are blue. All nice things are red. All nice, rough things are young. If something is nice then it is red. All rough things are young. If something is young then it is red.
The dog is red.
("dog" "is" "red" "+")
If something is blue and rough then it is nice.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If the dog is red then the dog is rough.
((("dog" "is" "red" "+")) -> ("dog" "is" "rough" "+"))
Red, rough things are blue.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All nice, rough things are young.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
The dog is red.
True
1
proof
[(triple1)]
("dog" "is" "red" "+")
triple1
The dog is not red.
False
1
inv-proof
[(triple1)]
("dog" "is" "red" "-")
triple1
The dog is rough.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "is" "rough" "-")
((triple1) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule7) OR ((((((triple1 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule5))]
("dog" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((triple1) -> (rule2 % int4))) -> (rule1 % int2)) ((triple1) -> (rule2 % int4))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
The dog is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("dog" "is" "blue" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is nice.
True
7
proof
[(((((triple1 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
("dog" "is" "nice" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog is not nice.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
("dog" "is" "nice" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
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 needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is red.[(triple1)] @1: The dog is rough.[(((triple1) -> rule2))] @2: The dog is blue.[(((triple1 ((triple1) -> rule2)) -> rule3))] The dog is young.[(((((triple1) -> rule2)) -> rule7) OR ((((((triple1 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule5))] @3: The dog is nice.[(((((triple1 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
The dog is red.
("dog" "is" "red" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((triple1) -> (rule2 % int4))) -> (rule1 % int2)) ((triple1) -> (rule2 % int4))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
The dog is nice.
("dog" "is" "nice" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3