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