The dog is kind. If something is kind then it is rough. All young, big things are kind. All rough, cold things are kind. All rough things are kind. Big things are young. If something is kind and rough then it is big.
The dog is kind.
("dog" "is" "kind" "+")
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All young, big things are kind.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All rough, cold things are kind.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is kind and rough then it is big.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
The dog is kind.
True
1
proof
[(triple1)]
("dog" "is" "kind" "+")
triple1
The dog is not kind.
False
1
inv-proof
[(triple1)]
("dog" "is" "kind" "-")
triple1
The dog is rough.
True
2
proof
[(((triple1) -> rule1))]
("dog" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is big.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule6))]
("dog" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule6))]
("dog" "is" "big" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is young.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule5))]
("dog" "is" "young" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule5))]
("dog" "is" "young" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
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 kind.[(triple1)] @1: The dog is rough.[(((triple1) -> rule1))] @2: The dog is big.[(((triple1 ((triple1) -> rule1)) -> rule6))] @3: The dog is young.[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule5))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3