Erin is smart. Erin is white. Fiona is nice. Gary is kind. Gary is nice. Harry is blue. Harry is smart. Kind, blue things are white. If Harry is kind then Harry is blue. Nice, white things are red. All white things are kind. If Harry is smart and Harry is young then Harry is blue. Kind things are nice.
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Kind, blue things are white.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Harry is kind then Harry is blue.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "blue" "+"))
Nice, white things are red.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If Harry is smart and Harry is young then Harry is blue.
((("Harry" "is" "smart" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "blue" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Erin is white.
True
1
proof
[(triple2)]
("Erin" "is" "white" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple6)]
("Harry" "is" "blue" "-")
triple6
Erin is kind.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("Erin" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("Erin" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
True
5
proof
[(((((((triple2) -> rule4)) -> rule6) triple2) -> rule3))]
("Erin" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not red.
False
5
inv-proof
[(((((((triple2) -> rule4)) -> rule6) triple2) -> rule3))]
("Erin" "is" "red" "-")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Harry is red.
Unknown
rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- FAIL)]]
("Harry" "is" "red" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Erin is smart.[(triple1)] Erin is white.[(triple2)] Fiona is nice.[(triple3)] Gary is kind.[(triple4)] Gary is nice.[(triple5 OR ((triple4) -> rule6))] Harry is blue.[(triple6)] Harry is smart.[(triple7)] @1: Erin is kind.[(((triple2) -> rule4))] @2: Erin is nice.[(((((triple2) -> rule4)) -> rule6))] @3: Erin is red.[(((((((triple2) -> rule4)) -> rule6) triple2) -> rule3))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
((triple4) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3