Erin is nice. Fiona is white. Gary is nice. Harry is white. Smart things are big. All young things are big. If something is nice then it is rough. White, smart things are rough. If something is rough and not nice then it is young. If something is big and not cold then it is not white.
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
White, smart things are rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is rough and not nice then it is young.
((("something" "is" "rough" "+") ("something" "is" "nice" "~")) -> ("something" "is" "young" "+"))
If something is big and not cold then it is not white.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "-"))
Fiona is white.
True
1
proof
[(triple2)]
("Fiona" "is" "white" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is rough.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "young" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Harry" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Erin is nice.[(triple1)] Fiona is white.[(triple2)] Gary is nice.[(triple3)] Harry is white.[(triple4)] @1: Erin is rough.[(((triple1) -> rule3))] Gary is rough.[(((triple3) -> rule3))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1