Bob is red. Dave is white. Fiona is white. Harry is quiet. If something is nice then it is smart. Kind, red things are nice. If Dave is red then Dave is kind. All blue things are kind. If something is quiet and red then it is nice. All smart things are red. Blue things are nice. Quiet things are blue.
Bob is red.
("Bob" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Kind, red things are nice.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Dave is red then Dave is kind.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "kind" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is quiet and red then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Fiona is not white.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "white" "-")
triple3
Harry is blue.
True
2
proof
[(((triple4) -> rule8))]
("Harry" "is" "blue" "+")
((triple4) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple4) -> rule8))]
("Harry" "is" "blue" "-")
((triple4) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
True
3
proof
[(((((triple4) -> rule8)) -> rule4))]
("Harry" "is" "kind" "+")
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule7))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple4) -> rule8)) -> rule7)) -> rule1))]
("Harry" "is" "smart" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule7)) -> rule1))]
("Harry" "is" "smart" "-")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@4: Dave is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule7 <- rule8 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "blue" "+")
Bob is not smart.
Unknown
inv-rconc
[@4: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- rule8 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is kind.
Unknown
rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is red.[(triple1)] Dave is white.[(triple2)] Fiona is white.[(triple3)] Harry is quiet.[(triple4)] @1: Harry is blue.[(((triple4) -> rule8))] @2: Harry is kind.[(((((triple4) -> rule8)) -> rule4))] Harry is nice.[(((((triple4) -> rule8)) -> rule7))] @3: Harry is smart.[(((((((triple4) -> rule8)) -> rule7)) -> rule1))] @4: Harry is red.[(((((((((triple4) -> rule8)) -> rule7)) -> rule1)) -> rule6))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((((triple4) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4