Dave is rough. Harry is red. If Dave is rough then Dave is not kind. If someone is white and not rough then they are round. All white people are round. If Harry is white and Harry is kind then Harry is round. Green, round people are red. All kind, rough people are smart. Red, round people are not smart. If Harry is red then Harry is white.
Dave is rough.
("Dave" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
If Dave is rough then Dave is not kind.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "kind" "-"))
If someone is white and not rough then they are round.
((("someone" "is" "white" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "round" "+"))
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Harry is white and Harry is kind then Harry is round.
((("Harry" "is" "white" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
Green, round people are red.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All kind, rough people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Red, round people are not smart.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "-"))
If Harry is red then Harry is white.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "white" "+"))
Harry is red.
True
1
proof
[(triple2)]
("Harry" "is" "red" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple1)]
("Dave" "is" "rough" "-")
triple1
Dave is not kind.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Harry is not white.
False
2
inv-proof
[(((triple2) -> rule8))]
("Harry" "is" "white" "-")
((triple2) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
True
3
proof
[(((((triple2) -> rule8)) -> rule3))]
("Harry" "is" "round" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule3))]
("Harry" "is" "round" "-")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not smart.
True
5
proof
[(((triple2 ((((triple2) -> rule8)) -> rule3)) -> rule7))]
("Harry" "is" "smart" "-")
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is smart.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule8)) -> rule3)) -> rule7))]
("Harry" "is" "smart" "+")
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is rough.[(triple1)] Harry is red.[(triple2)] @1: Dave is not kind.[(((triple1) -> rule1))] Harry is white.[(((triple2) -> rule8))] @2: Harry is round.[(((((triple2) -> rule8)) -> rule3))] @3: Harry is not smart.[(((triple2 ((((triple2) -> rule8)) -> rule3)) -> rule7))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple2) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3