Anne is not blue. Anne is not cold. Anne is green. Anne is nice. Anne is quiet. Charlie is big. Charlie is blue. Charlie is not quiet. Charlie is rough. Erin is big. Erin is quiet. Erin is rough. Harry is big. Harry is cold. Harry is quiet. If Charlie is not cold then Charlie is not nice. All cold, quiet things are nice. Big things are nice. All nice, big things are blue. If Anne is rough then Anne is quiet. If something is quiet and not cold then it is green. If something is green and cold then it is quiet. Green things are rough.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Charlie is not cold then Charlie is not nice.
((("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "nice" "-"))
All cold, quiet things are nice.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All nice, big things are blue.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If Anne is rough then Anne is quiet.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "quiet" "+"))
If something is quiet and not cold then it is green.
((("something" "is" "quiet" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "+"))
If something is green and cold then it is quiet.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Harry is cold.
True
1
proof
[(triple14)]
("Harry" "is" "cold" "+")
triple14
Charlie is not blue.
False
1
inv-proof
[(triple7 OR ((((triple6) -> rule3) triple6) -> rule4))]
("Charlie" "is" "blue" "-")
triple7
((((triple6) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is nice.
True
2
proof
[(((triple6) -> rule3))]
("Charlie" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple10) -> rule3))]
("Erin" "is" "nice" "-")
((triple10) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule4))]
("Erin" "is" "blue" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule4))]
("Erin" "is" "blue" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is green.[(triple3 OR ((triple5 triple2) -> rule6))] Anne is nice.[(triple4)] Anne is not blue.[(triple1)] Anne is not cold.[(triple2)] Anne is quiet.[(triple5 OR ((((triple3) -> rule8)) -> rule5))] Charlie is big.[(triple6)] Charlie is blue.[(triple7 OR ((((triple6) -> rule3) triple6) -> rule4))] Charlie is not quiet.[(triple8)] Charlie is rough.[(triple9)] Erin is big.[(triple10)] Erin is quiet.[(triple11)] Erin is rough.[(triple12)] Harry is big.[(triple13)] Harry is cold.[(triple14)] Harry is quiet.[(triple15)] @1: Anne is rough.[(((triple3) -> rule8) OR ((((triple5 triple2) -> rule6)) -> rule8))] Charlie is nice.[(((triple6) -> rule3))] Erin is nice.[(((triple10) -> rule3))] Harry is nice.[(((triple13) -> rule3) OR ((triple14 triple15) -> rule2))] @2: Erin is blue.[(((((triple10) -> rule3) triple10) -> rule4))] Harry is blue.[(((((triple13) -> rule3) triple13) -> rule4) OR ((((triple14 triple15) -> rule2) triple13) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple5 triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
((((triple6) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is cold.
("Harry" "is" "cold" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Anne is rough.
("Anne" "is" "rough" "+")
((triple3) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple5 triple2) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple13) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple14 triple15) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple13) -> (rule3 % int2)) triple13) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple14 triple15) -> (rule2 % int2)) triple13) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2