Anne is quiet. Anne is rough. Charlie is kind. Fiona is green. Fiona is rough. Harry is green. Harry is kind. Harry is nice. Harry is rough. Harry is white. All nice, rough things are white. All rough things are quiet. Rough, green things are quiet. If something is white then it is nice. If something is nice and rough then it is quiet. Kind things are green.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All nice, rough things are white.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Rough, green things are quiet.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is nice and rough then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple8 OR ((triple10) -> rule4))]
("Harry" "is" "nice" "+")
triple8
((triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple8 OR ((triple10) -> rule4))]
("Harry" "is" "nice" "-")
triple8
((triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Fiona is quiet.
True
2
proof
[(((triple5) -> rule2) OR ((triple5 triple4) -> rule3))]
("Fiona" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple5 triple4) -> rule3))]
("Fiona" "is" "quiet" "-")
((triple5) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is quiet.[(triple1 OR ((triple2) -> rule2))] Anne is rough.[(triple2)] Charlie is kind.[(triple3)] Fiona is green.[(triple4)] Fiona is rough.[(triple5)] Harry is green.[(triple6 OR ((triple7) -> rule6))] Harry is kind.[(triple7)] Harry is nice.[(triple8 OR ((triple10) -> rule4))] Harry is rough.[(triple9)] Harry is white.[(triple10 OR ((triple8 triple9) -> rule1))] @1: Charlie is green.[(((triple3) -> rule6))] Fiona is quiet.[(((triple5) -> rule2) OR ((triple5 triple4) -> rule3))] Harry is quiet.[(((triple9) -> rule2) OR ((triple8 triple9) -> rule5) OR ((triple9 triple6) -> rule3) OR ((triple9 ((triple7) -> rule6)) -> rule3) OR ((((triple10) -> rule4) triple9) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
((triple7) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple8 triple9) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8 triple9) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple9 triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple9 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple10) -> (rule4 % int2)) triple9) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2