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