Dave is not round. Erin is not white. Fiona is not young. Harry is rough. Rough things are kind. If Dave is nice then Dave is not rough. Round things are blue. Kind things are round. Young things are round. If Erin is not nice and Erin is not round then Erin is blue.
Dave is not round.
("Dave" "is" "round" "-")
Erin is not white.
("Erin" "is" "white" "-")
Fiona is not young.
("Fiona" "is" "young" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Dave is nice then Dave is not rough.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "rough" "-"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If Erin is not nice and Erin is not round then Erin is blue.
((("Erin" "is" "nice" "~") ("Erin" "is" "round" "~")) -> ("Erin" "is" "blue" "+"))
Fiona is not young.
True
1
proof
[(triple3)]
("Fiona" "is" "young" "-")
triple3
Fiona is young.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "young" "+")
triple3
Harry is kind.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
True
3
proof
[(((((triple4) -> rule1)) -> rule4))]
("Harry" "is" "round" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("Harry" "is" "round" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
True
4
proof
[(((((((triple4) -> rule1)) -> rule4)) -> rule3))]
("Harry" "is" "blue" "+")
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not blue.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule4)) -> rule3))]
("Harry" "is" "blue" "-")
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Erin is blue.
Unknown
rconc
[@3: Erin is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is not round.[(triple1)] Erin is not white.[(triple2)] Fiona is not young.[(triple3)] Harry is rough.[(triple4)] @1: Harry is kind.[(((triple4) -> rule1))] @2: Harry is round.[(((((triple4) -> rule1)) -> rule4))] @3: Harry is blue.[(((((((triple4) -> rule1)) -> rule4)) -> rule3))]
Dave is not round.
("Dave" "is" "round" "-")
triple1
Erin is not white.
("Erin" "is" "white" "-")
triple2
Fiona is not young.
("Fiona" "is" "young" "-")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3