Charlie is not cold. Charlie is rough. Fiona is green. Fiona is rough. Fiona is round. Gary is rough. Gary is not smart. Harry is quiet. Harry is rough. Harry is smart. If someone is round and nice then they are rough. If someone is nice and cold then they are rough. If someone is smart and rough then they are not cold. All quiet, green people are round. If someone is rough and quiet then they are green. If someone is round then they are quiet. If Charlie is cold and Charlie is not smart then Charlie is quiet. If Gary is green then Gary is not quiet.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is round and nice then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice and cold then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and rough then they are not cold.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "-"))
All quiet, green people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and quiet then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is cold and Charlie is not smart then Charlie is quiet.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "smart" "~")) -> ("Charlie" "is" "quiet" "+"))
If Gary is green then Gary is not quiet.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "quiet" "-"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Gary is smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "+")
triple7
Harry is green.
True
3
proof
[(((triple9 triple8) -> rule5))]
("Harry" "is" "green" "+")
((triple9 triple8) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
False
3
inv-proof
[(((triple10 triple9) -> rule3))]
("Harry" "is" "cold" "+")
((triple10 triple9) -> (rule3 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is round.
True
5
proof
[(((triple8 ((triple9 triple8) -> rule5)) -> rule4))]
("Harry" "is" "round" "+")
((triple8 ((triple9 triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not round.
False
5
inv-proof
[(((triple8 ((triple9 triple8) -> rule5)) -> rule4))]
("Harry" "is" "round" "-")
((triple8 ((triple9 triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is green.
Unknown
rconc
[@3: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is not cold.[(triple1)] Charlie is rough.[(triple2)] Fiona is green.[(triple3 OR ((triple4 ((triple5) -> rule6)) -> rule5))] Fiona is rough.[(triple4)] Fiona is round.[(triple5)] Gary is not smart.[(triple7)] Gary is rough.[(triple6)] Harry is quiet.[(triple8)] Harry is rough.[(triple9)] Harry is smart.[(triple10)] @1: Fiona is quiet.[(((triple5) -> rule6))] Harry is green.[(((triple9 triple8) -> rule5))] Harry is not cold.[(((triple10 triple9) -> rule3))] @2: Harry is round.[(((triple8 ((triple9 triple8) -> rule5)) -> rule4))]
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
((triple4 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Gary is not smart.
("Gary" "is" "smart" "-")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple5) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple9 triple8) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple10 triple9) -> (rule3 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple8 ((triple9 triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2