Charlie is quiet. Charlie is not white. Charlie is not young. Fiona is blue. Fiona is nice. Fiona is rough. Fiona is not round. Fiona is white. Fiona is young. Harry is rough. Harry is white. Harry is young. If someone is round and not young then they are not white. Round people are white. If someone is nice and not young then they are not rough. If someone is round and not white then they are rough. If Harry is blue and Harry is rough then Harry is not quiet. All quiet people are nice.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is not young.
("Charlie" "is" "young" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is round and not young then they are not white.
((("someone" "is" "round" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "-"))
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and not young then they are not rough.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "-"))
If someone is round and not white then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
If Harry is blue and Harry is rough then Harry is not quiet.
((("Harry" "is" "blue" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "quiet" "-"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Fiona is rough.
True
1
proof
[(triple6)]
("Fiona" "is" "rough" "+")
triple6
Fiona is not rough.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "rough" "-")
triple6
Charlie is nice.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not rough.
True
4
proof
[(((((triple1) -> rule6) triple3) -> rule3))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
False
4
inv-proof
[(((((triple1) -> rule6) triple3) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Charlie is not white.[(triple2)] Charlie is not young.[(triple3)] Charlie is quiet.[(triple1)] Fiona is blue.[(triple4)] Fiona is nice.[(triple5)] Fiona is not round.[(triple7)] Fiona is rough.[(triple6)] Fiona is white.[(triple8)] Fiona is young.[(triple9)] Harry is rough.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12)] @1: Charlie is nice.[(((triple1) -> rule6))] @2: Charlie is not rough.[(((((triple1) -> rule6) triple3) -> rule3))]
Charlie is not white.
("Charlie" "is" "white" "-")
triple2
Charlie is not young.
("Charlie" "is" "young" "-")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is not round.
("Fiona" "is" "round" "-")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
((((triple1) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2