Bob is blue. Harry is blue. Harry is green. All green, blue people are big. Big people are round. All rough, green people are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
All green, blue people are big.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All rough, green people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Harry is blue.
True
1
proof
[(triple2)]
("Harry" "is" "blue" "+")
triple2
Harry is not blue.
False
1
inv-proof
[(triple2)]
("Harry" "is" "blue" "-")
triple2
Harry is big.
True
3
proof
[(((triple3 triple2) -> rule1))]
("Harry" "is" "big" "+")
((triple3 triple2) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("Harry" "is" "big" "-")
((triple3 triple2) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
True
4
proof
[(((((triple3 triple2) -> rule1)) -> rule2))]
("Harry" "is" "round" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not round.
False
4
inv-proof
[(((((triple3 triple2) -> rule1)) -> rule2))]
("Harry" "is" "round" "-")
((((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Harry is blue.[(triple2)] Harry is green.[(triple3)] @1: Harry is big.[(((triple3 triple2) -> rule1))] @2: Harry is round.[(((((triple3 triple2) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3 triple2) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2