The dog is rough. If someone is nice then they are rough. Nice, big people are kind. If someone is rough then they are kind. Rough, kind people are nice. If someone is nice then they are blue. Blue people are rough. If someone is big then they are kind. All blue people are big.
The dog is rough.
("dog" "is" "rough" "+")
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Nice, big people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Rough, kind people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule3))]
("dog" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("dog" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is nice.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule4))]
("dog" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule4))]
("dog" "is" "nice" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
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 eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog is rough.[(triple1)] @1: The dog is kind.[(((triple1) -> rule3))] @2: The dog is nice.[(((triple1 ((triple1) -> rule3)) -> rule4))] @3: The dog is blue.[(((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5))] @4: The dog is big.[(((((((triple1 ((triple1) -> rule3)) -> rule4)) -> rule5)) -> rule8))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog is big.
("dog" "is" "big" "+")
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4