Harry is round. If something is big and round then it is green. If Harry is round then Harry is cold. All round, young things are big. If something is round then it is young. All smart, big things are round. If Harry is furry then Harry is smart. If Harry is young and Harry is round then Harry is cold. If something is smart then it is young.
Harry is round.
("Harry" "is" "round" "+")
If something is big and round then it is green.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If Harry is round then Harry is cold.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "cold" "+"))
All round, young things are big.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All smart, big things are round.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Harry is furry then Harry is smart.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "smart" "+"))
If Harry is young and Harry is round then Harry is cold.
((("Harry" "is" "young" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "cold" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Harry is round.
True
1
proof
[(triple1)]
("Harry" "is" "round" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple1)]
("Harry" "is" "round" "-")
triple1
Harry is young.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "young" "+")
((triple1) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule7))]
("Harry" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Harry" "is" "big" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Harry" "is" "big" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
True
6
proof
[(((((triple1 ((triple1) -> rule4)) -> rule3) triple1) -> rule1))]
("Harry" "is" "green" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not green.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule3) triple1) -> rule1))]
("Harry" "is" "green" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Harry is round.[(triple1)] @1: Harry is cold.[(((triple1) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule7))] Harry is young.[(((triple1) -> rule4))] @2: Harry is big.[(((triple1 ((triple1) -> rule4)) -> rule3))] @3: Harry is green.[(((((triple1 ((triple1) -> rule4)) -> rule3) triple1) -> rule1))]
Harry is round.
("Harry" "is" "round" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple1) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3