The dog is rough. If something is rough then it is young. Cold things are kind. Kind, young things are cold. If the dog is blue and the dog is kind then the dog is rough. All cold, young things are rough. Young things are kind. If something is blue and kind then it is cold. If the dog is cold then the dog is rough.
The dog is rough.
("dog" "is" "rough" "+")
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Kind, young things are cold.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If the dog is blue and the dog is kind then the dog is rough.
((("dog" "is" "blue" "+") ("dog" "is" "kind" "+")) -> ("dog" "is" "rough" "+"))
All cold, young things are rough.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is blue and kind then it is cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If the dog is cold then the dog is rough.
((("dog" "is" "cold" "+")) -> ("dog" "is" "rough" "+"))
The dog is rough.
True
1
proof
[(triple1)]
("dog" "is" "rough" "+")
triple1
The dog is not rough.
False
1
inv-proof
[(triple1)]
("dog" "is" "rough" "-")
triple1
The dog is young.
True
2
proof
[(((triple1) -> rule1))]
("dog" "is" "young" "+")
((triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "is" "young" "-")
((triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("dog" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("dog" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is cold.
True
6
proof
[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule3))]
("dog" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog is not cold.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule3))]
("dog" "is" "cold" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
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 is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The dog is rough.[(triple1)] @1: The dog is young.[(((triple1) -> rule1))] @2: The dog is kind.[(((((triple1) -> rule1)) -> rule6))] @3: The dog is cold.[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule3))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
((triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3