Charlie is blue. Fiona is nice. Gary is blue. Harry is rough. Nice things are blue. If something is rough then it is red. All rough things are blue. All blue, nice things are rough. If Gary is green then Gary is rough. All red, green things are nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All blue, nice things are rough.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Gary is green then Gary is rough.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "rough" "+"))
All red, green things are nice.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Fiona is not nice.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "nice" "-")
triple2
Harry is blue.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "red" "-")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Fiona is rough.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule4))]
("Fiona" "is" "rough" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not rough.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule4))]
("Fiona" "is" "rough" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is red.
True
5
proof
[(((((((triple2) -> rule1) triple2) -> rule4)) -> rule2))]
("Fiona" "is" "red" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not red.
False
5
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule4)) -> rule2))]
("Fiona" "is" "red" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("Gary" "is" "red" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is rough.
Unknown
rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "rough" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Fiona is nice.[(triple2)] Gary is blue.[(triple3)] Harry is rough.[(triple4)] @1: Fiona is blue.[(((triple2) -> rule1))] Harry is blue.[(((triple4) -> rule3))] Harry is red.[(((triple4) -> rule2))] @2: Fiona is rough.[(((((triple2) -> rule1) triple2) -> rule4))] @3: Fiona is red.[(((((((triple2) -> rule1) triple2) -> rule4)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3