Dave is cold. If Dave is quiet then Dave is young. If Dave is not smart then Dave is young. All furry, green things are not quiet. All green things are not young. White things are green. All cold things are white. Young things are white. All young, white things are furry.
Dave is cold.
("Dave" "is" "cold" "+")
If Dave is quiet then Dave is young.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "young" "+"))
If Dave is not smart then Dave is young.
((("Dave" "is" "smart" "~")) -> ("Dave" "is" "young" "+"))
All furry, green things are not quiet.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "-"))
All green things are not young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "-"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
All young, white things are furry.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is white.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "white" "+")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple1) -> rule6))]
("Dave" "is" "white" "-")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("Dave" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("Dave" "is" "green" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not young.
True
4
proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule4))]
("Dave" "is" "young" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule4))]
("Dave" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is cold.[(triple1)] @1: Dave is white.[(((triple1) -> rule6))] @2: Dave is green.[(((((triple1) -> rule6)) -> rule5))] @3: Dave is not young.[(((((((triple1) -> rule6)) -> rule5)) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not young.
("Dave" "is" "young" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3