Anne is green. Dave is cold. Fiona is green. Harry is cold. All blue things are big. Quiet things are not nice. Blue things are not green. White, cold things are not green. If something is cold then it is quiet. If Anne is white and Anne is big then Anne is not cold. All green things are not white. If something is big and white then it is blue.
Anne is green.
("Anne" "is" "green" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Quiet things are not nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
Blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
White, cold things are not green.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "-"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Anne is white and Anne is big then Anne is not cold.
((("Anne" "is" "white" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "cold" "-"))
All green things are not white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "-"))
If something is big and white then it is blue.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Harry is cold.
True
1
proof
[(triple4)]
("Harry" "is" "cold" "+")
triple4
Dave is not cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "-")
triple2
Harry is quiet.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is white.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "white" "+")
((triple1) -> (rule7 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Harry is not nice.
True
3
proof
[(((((triple4) -> rule5)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Dave is nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Harry" "is" "big" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Anne" "is" "big" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is green.[(triple1)] Dave is cold.[(triple2)] Fiona is green.[(triple3)] Harry is cold.[(triple4)] @1: Anne is not white.[(((triple1) -> rule7))] Dave is quiet.[(((triple2) -> rule5))] Fiona is not white.[(((triple3) -> rule7))] Harry is quiet.[(((triple4) -> rule5))] @2: Dave is not nice.[(((((triple2) -> rule5)) -> rule2))] Harry is not nice.[(((((triple4) -> rule5)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Anne is not white.
("Anne" "is" "white" "-")
((triple1) -> (rule7 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is not white.
("Fiona" "is" "white" "-")
((triple3) -> (rule7 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2