Charlie is cold. Charlie is not nice. Charlie is smart. Dave is white. Fiona is blue. Fiona is not kind. Harry is kind. If Fiona is white then Fiona is not red. If something is nice and not kind then it is smart. Blue, nice things are smart. If something is red then it is cold. If something is kind then it is blue. If Dave is red and Dave is smart then Dave is blue. Kind, cold things are white. Blue things are red. Kind, white things are not nice.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Harry is kind.
("Harry" "is" "kind" "+")
If Fiona is white then Fiona is not red.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "red" "-"))
If something is nice and not kind then it is smart.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "smart" "+"))
Blue, nice things are smart.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Dave is red and Dave is smart then Dave is blue.
((("Dave" "is" "red" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "blue" "+"))
Kind, cold things are white.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Kind, white things are not nice.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
Dave is white.
True
1
proof
[(triple4)]
("Dave" "is" "white" "+")
triple4
Charlie is not smart.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "smart" "-")
triple3
Fiona is red.
True
2
proof
[(((triple5) -> rule8))]
("Fiona" "is" "red" "+")
((triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple5) -> rule8))]
("Fiona" "is" "red" "-")
((triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple5) -> rule8)) -> rule4))]
("Fiona" "is" "cold" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule4))]
("Fiona" "is" "cold" "-")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is cold.
True
4
proof
[(((((((triple7) -> rule5)) -> rule8)) -> rule4))]
("Harry" "is" "cold" "+")
((((((triple7) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not cold.
False
4
inv-proof
[(((((((triple7) -> rule5)) -> rule8)) -> rule4))]
("Harry" "is" "cold" "-")
((((((triple7) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
True
6
proof
[(((triple7 ((((((triple7) -> rule5)) -> rule8)) -> rule4)) -> rule7))]
("Harry" "is" "white" "+")
((triple7 ((((((triple7) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not white.
False
6
inv-proof
[(((triple7 ((((((triple7) -> rule5)) -> rule8)) -> rule4)) -> rule7))]
("Harry" "is" "white" "-")
((triple7 ((((((triple7) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not nice.
True
8
proof
[(((triple7 ((triple7 ((((((triple7) -> rule5)) -> rule8)) -> rule4)) -> rule7)) -> rule9))]
("Harry" "is" "nice" "-")
((triple7 ((triple7 ((((((triple7) -> (rule5 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
int5
Harry is nice.
False
8
inv-proof
[(((triple7 ((triple7 ((((((triple7) -> rule5)) -> rule8)) -> rule4)) -> rule7)) -> rule9))]
("Harry" "is" "nice" "+")
((triple7 ((triple7 ((((((triple7) -> (rule5 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
int5
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "white" "+")
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Dave" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Charlie" "is" "red" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is cold.[(triple1)] Charlie is not nice.[(triple2)] Charlie is smart.[(triple3)] Dave is white.[(triple4)] Fiona is blue.[(triple5)] Fiona is not kind.[(triple6)] Harry is kind.[(triple7)] @1: Fiona is red.[(((triple5) -> rule8))] Harry is blue.[(((triple7) -> rule5))] @2: Fiona is cold.[(((((triple5) -> rule8)) -> rule4))] Harry is red.[(((((triple7) -> rule5)) -> rule8))] @3: Harry is cold.[(((((((triple7) -> rule5)) -> rule8)) -> rule4))] @4: Harry is white.[(((triple7 ((((((triple7) -> rule5)) -> rule8)) -> rule4)) -> rule7))] @5: Harry is not nice.[(((triple7 ((triple7 ((((((triple7) -> rule5)) -> rule8)) -> rule4)) -> rule7)) -> rule9))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
((triple5) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple7) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple7 ((((((triple7) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not nice.
("Harry" "is" "nice" "-")
((triple7 ((triple7 ((((((triple7) -> (rule5 % int5))) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
int5