Dave is nice. Harry is blue. All blue things are red. If Dave is green and Dave is red then Dave is nice. Quiet, blue things are rough. If Harry is smart then Harry is blue. Blue, red things are quiet. If something is nice and smart then it is quiet.
Dave is nice.
("Dave" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If Dave is green and Dave is red then Dave is nice.
((("Dave" "is" "green" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "nice" "+"))
Quiet, blue things are rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Harry is smart then Harry is blue.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "blue" "+"))
Blue, red things are quiet.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is nice and smart then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
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 red.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "red" "+")
((triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("Harry" "is" "red" "-")
((triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule5))]
("Harry" "is" "quiet" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule5))]
("Harry" "is" "quiet" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
True
6
proof
[(((((triple2 ((triple2) -> rule1)) -> rule5) triple2) -> rule3))]
("Harry" "is" "rough" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not rough.
False
6
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule5) triple2) -> rule3))]
("Harry" "is" "rough" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is nice.[(triple1)] Harry is blue.[(triple2)] @1: Harry is red.[(((triple2) -> rule1))] @2: Harry is quiet.[(((triple2 ((triple2) -> rule1)) -> rule5))] @3: Harry is rough.[(((((triple2 ((triple2) -> rule1)) -> rule5) triple2) -> rule3))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3