Anne is green. Anne is smart. Dave is blue. Dave is cold. Dave is smart. Dave is white. Fiona is blue. Fiona is smart. Fiona is white. Harry is cold. If Fiona is white then Fiona is quiet. Quiet things are blue. Green things are quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Fiona is white then Fiona is quiet.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "quiet" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Dave is blue.
True
1
proof
[(triple3)]
("Dave" "is" "blue" "+")
triple3
Dave is not cold.
False
1
inv-proof
[(triple4)]
("Dave" "is" "cold" "-")
triple4
Anne is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple9) -> rule1))]
("Fiona" "is" "quiet" "-")
((triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is green.[(triple1)] Anne is smart.[(triple2)] Dave is blue.[(triple3)] Dave is cold.[(triple4)] Dave is smart.[(triple5)] Dave is white.[(triple6)] Fiona is blue.[(triple7 OR ((((triple9) -> rule1)) -> rule2))] Fiona is smart.[(triple8)] Fiona is white.[(triple9)] Harry is cold.[(triple10)] @1: Anne is quiet.[(((triple1) -> rule3))] Fiona is quiet.[(((triple9) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule3)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple9) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2