Dave is red. Erin is nice. Fiona is young. Nice things are young. All cold, round things are red. If Fiona is nice then Fiona is blue. If something is green and nice then it is young. If something is young then it is round. If something is round then it is nice.
Dave is red.
("Dave" "is" "red" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All cold, round things are red.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If Fiona is nice then Fiona is blue.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "blue" "+"))
If something is green and nice then it is young.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Erin is not nice.
False
1
inv-proof
[(triple2)]
("Erin" "is" "nice" "-")
triple2
Fiona is round.
True
2
proof
[(((triple3) -> rule5))]
("Fiona" "is" "round" "+")
((triple3) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "young" "-")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple3) -> rule5)) -> rule6))]
("Fiona" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule6))]
("Fiona" "is" "nice" "-")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "+")
Dave is not round.
Unknown
inv-rconc
[@3: Dave is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is red.[(triple1)] Erin is nice.[(triple2)] Fiona is young.[(triple3)] @1: Erin is young.[(((triple2) -> rule1))] Fiona is round.[(((triple3) -> rule5))] @2: Erin is round.[(((((triple2) -> rule1)) -> rule5))] Fiona is nice.[(((((triple3) -> rule5)) -> rule6))] @3: Fiona is blue.[(((((((triple3) -> rule5)) -> rule6)) -> rule3))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Erin is young.
("Erin" "is" "young" "+")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3