Charlie is smart. Fiona is green. Harry is rough. If Harry is not smart then Harry is not rough. If someone is big and not smart then they are green. If someone is rough then they are white. If someone is big and rough then they are not white. Big, green people are kind. If Charlie is smart then Charlie is rough.
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is not smart then Harry is not rough.
((("Harry" "is" "smart" "~")) -> ("Harry" "is" "rough" "-"))
If someone is big and not smart then they are green.
((("someone" "is" "big" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "green" "+"))
If someone is rough then they are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is big and rough then they are not white.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
Big, green people are kind.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is smart then Charlie is rough.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "rough" "+"))
Fiona is green.
True
1
proof
[(triple2)]
("Fiona" "is" "green" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Harry is white.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "+")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "-")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is smart.[(triple1)] Fiona is green.[(triple2)] Harry is rough.[(triple3)] @1: Charlie is rough.[(((triple1) -> rule6))] Harry is white.[(((triple3) -> rule3))] @2: Charlie is white.[(((((triple1) -> rule6)) -> rule3))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2