Bob is kind. Fiona is smart. Gary is rough. Harry is green. Smart people are rough. If someone is round and kind then they are rough. Rough people are round.
Bob is kind.
("Bob" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is green.
("Harry" "is" "green" "+")
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is round and kind then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Fiona is smart.
True
1
proof
[(triple2)]
("Fiona" "is" "smart" "+")
triple2
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is round.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "round" "+")
((triple3) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "round" "-")
((triple3) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Fiona is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Fiona" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Fiona" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not rough.
Unknown
inv-rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is kind.[(triple1)] Fiona is smart.[(triple2)] Gary is rough.[(triple3)] Harry is green.[(triple4)] @1: Fiona is rough.[(((triple2) -> rule1))] Gary is round.[(((triple3) -> rule3))] @2: Fiona is round.[(((((triple2) -> rule1)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2