Harry is young. Nice things are rough. All young things are nice. Green, quiet things are red. All nice, rough things are cold. If something is nice then it is rough. If Harry is red then Harry is rough. Young things are nice. Young, nice things are quiet.
Harry is young.
("Harry" "is" "young" "+")
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Green, quiet things are red.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All nice, rough things are cold.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Harry is red then Harry is rough.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "rough" "+"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Young, nice things are quiet.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Harry is young.
True
1
proof
[(triple1)]
("Harry" "is" "young" "+")
triple1
Harry is not young.
False
1
inv-proof
[(triple1)]
("Harry" "is" "young" "-")
triple1
Harry is nice.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule7))]
("Harry" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple1) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule7))]
("Harry" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple1) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule8))]
("Harry" "is" "quiet" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1) OR ((((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule7)) -> rule1) OR ((((triple1) -> rule7)) -> rule5))]
("Harry" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Harry is young.[(triple1)] @1: Harry is nice.[(((triple1) -> rule2) OR ((triple1) -> rule7))] @2: Harry is quiet.[(((triple1 ((triple1) -> rule2)) -> rule8) OR ((triple1 ((triple1) -> rule7)) -> rule8))] Harry is rough.[(((((triple1) -> rule2)) -> rule1) OR ((((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule7)) -> rule1) OR ((((triple1) -> rule7)) -> rule5))] @3: Harry is cold.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule5)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule7)) -> rule1)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule7)) -> rule5)) -> rule4) OR ((((triple1) -> rule7) ((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((triple1) -> rule7) ((((triple1) -> rule2)) -> rule5)) -> rule4) OR ((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule4) OR ((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule5)) -> rule4))]
Harry is young.
("Harry" "is" "young" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple1) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3