Bob is red. Fiona is red. Gary is white. Harry is red. If something is nice and rough then it is white. If Fiona is not quiet then Fiona is not nice. If something is furry and red then it is rough. Red things are nice. White, quiet things are red. If something is red and not nice then it is blue. If something is nice then it is not blue. If something is white and red then it is blue.
Bob is red.
("Bob" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is nice and rough then it is white.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Fiona is not quiet then Fiona is not nice.
((("Fiona" "is" "quiet" "~")) -> ("Fiona" "is" "nice" "-"))
If something is furry and red then it is rough.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
White, quiet things are red.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is red and not nice then it is blue.
((("something" "is" "red" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "+"))
If something is nice then it is not blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "-"))
If something is white and red then it is blue.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Fiona is not red.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "red" "-")
triple2
Harry is nice.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "nice" "+")
((triple4) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "white" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "white" "+")
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Bob is red.[(triple1)] Fiona is red.[(triple2)] Gary is white.[(triple3)] Harry is red.[(triple4)] @1: Bob is nice.[(((triple1) -> rule4))] Fiona is nice.[(((triple2) -> rule4))] Harry is nice.[(((triple4) -> rule4))] @2: Bob is not blue.[(((((triple1) -> rule4)) -> rule7))] Fiona is not blue.[(((((triple2) -> rule4)) -> rule7))] Harry is not blue.[(((((triple4) -> rule4)) -> rule7))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple4) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2