Charlie is smart. Dave is smart. Fiona is blue. Harry is quiet. If something is quiet then it is cold. If something is quiet and cold then it is blue.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is quiet and cold then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Fiona is not blue.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "blue" "-")
triple3
Harry is cold.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "cold" "-")
((triple4) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("Harry" "is" "blue" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("Harry" "is" "blue" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is smart.[(triple1)] Dave is smart.[(triple2)] Fiona is blue.[(triple3)] Harry is quiet.[(triple4)] @1: Harry is cold.[(((triple4) -> rule1))] @2: Harry is blue.[(((triple4 ((triple4) -> rule1)) -> rule2))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2