Bob is quiet. Harry is quiet. Harry is round. If Harry is round then Harry is big. If something is nice and round then it is furry. All rough things are nice. Quiet, big things are rough. Nice things are big. Nice things are round.
Bob is quiet.
("Bob" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is round then Harry is big.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "+"))
If something is nice and round then it is furry.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Quiet, big things are rough.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple3)]
("Harry" "is" "round" "-")
triple3
Harry is big.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "big" "-")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
True
4
proof
[(((triple2 ((triple3) -> rule1)) -> rule4))]
("Harry" "is" "rough" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((triple2 ((triple3) -> rule1)) -> rule4))]
("Harry" "is" "rough" "-")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
True
5
proof
[(((((triple2 ((triple3) -> rule1)) -> rule4)) -> rule3))]
("Harry" "is" "nice" "+")
((((triple2 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not nice.
False
5
inv-proof
[(((((triple2 ((triple3) -> rule1)) -> rule4)) -> rule3))]
("Harry" "is" "nice" "-")
((((triple2 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is furry.
Unknown
rconc
[@4: Bob is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule4 <- rule5 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not big.
Unknown
inv-rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule4 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is rough.
Unknown
rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Harry is quiet.[(triple2)] Harry is round.[(triple3)] @1: Harry is big.[(((triple3) -> rule1))] @2: Harry is rough.[(((triple2 ((triple3) -> rule1)) -> rule4))] @3: Harry is nice.[(((((triple2 ((triple3) -> rule1)) -> rule4)) -> rule3))] @4: Harry is furry.[(((((((triple2 ((triple3) -> rule1)) -> rule4)) -> rule3) triple3) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple2 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple2 ((triple3) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4