Dave is smart. Fiona is not round. If Dave is smart then Dave is red. If someone is red then they are cold. All round, red people are cold. If someone is nice then they are not round. All cold people are round. If someone is round and not furry then they are red. If Dave is smart and Dave is not cold then Dave is not blue. If someone is round and not red then they are not blue.
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
If Dave is smart then Dave is red.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "red" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All round, red people are cold.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are not round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "-"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is round and not furry then they are red.
((("someone" "is" "round" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "red" "+"))
If Dave is smart and Dave is not cold then Dave is not blue.
((("Dave" "is" "smart" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "blue" "-"))
If someone is round and not red then they are not blue.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "blue" "-"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Fiona is round.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "round" "+")
triple2
Dave is red.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "red" "+")
((triple1) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "red" "-")
((triple1) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Dave" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not round.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Dave" "is" "round" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Dave is smart.[(triple1)] Fiona is not round.[(triple2)] @1: Dave is red.[(((triple1) -> rule1))] @2: Dave is cold.[(((((triple1) -> rule1)) -> rule2))] @3: Dave is round.[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Fiona is not round.
("Fiona" "is" "round" "-")
triple2
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3