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