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