The dog is rough. If the dog is rough and the dog is not blue then the dog is red. Round people are kind. If the dog is rough then the dog is round. If the dog is blue and the dog is not round then the dog is kind. Kind people are red. If someone is blue and rough then they are red.
The dog is rough.
("dog" "is" "rough" "+")
If the dog is rough and the dog is not blue then the dog is red.
((("dog" "is" "rough" "+") ("dog" "is" "blue" "~")) -> ("dog" "is" "red" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If the dog is rough then the dog is round.
((("dog" "is" "rough" "+")) -> ("dog" "is" "round" "+"))
If the dog is blue and the dog is not round then the dog is kind.
((("dog" "is" "blue" "+") ("dog" "is" "round" "~")) -> ("dog" "is" "kind" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and rough then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
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 round.
True
2
proof
[(((triple1) -> rule3))]
("dog" "is" "round" "+")
((triple1) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("dog" "is" "round" "-")
((triple1) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("dog" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("dog" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is red.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("dog" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The dog is not red.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("dog" "is" "red" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
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 visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
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 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 round.[(((triple1) -> rule3))] @2: The dog is kind.[(((((triple1) -> rule3)) -> rule2))] @3: The dog is red.[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is red.
("dog" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3