Anne is young. Dave is young. Fiona is cold. If someone is kind then they are young. If someone is blue then they are round. Kind people are blue. If Dave is round then Dave is smart. If someone is smart then they are blue. If Dave is young then Dave is blue. If someone is round then they are cold. If someone is cold and kind then they are red.
Anne is young.
("Anne" "is" "young" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Dave is round then Dave is smart.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "smart" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Dave is young then Dave is blue.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "blue" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and kind then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Dave is young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple2)]
("Dave" "is" "young" "-")
triple2
Dave is blue.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("Dave" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("Dave" "is" "round" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
("Dave" "is" "smart" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
("Dave" "is" "smart" "-")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "red" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "red" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "round" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is young.[(triple1)] Dave is young.[(triple2)] Fiona is cold.[(triple3)] @1: Dave is blue.[(((triple2) -> rule6))] @2: Dave is round.[(((((triple2) -> rule6)) -> rule2))] @3: Dave is cold.[(((((((triple2) -> rule6)) -> rule2)) -> rule7))] Dave is smart.[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3