Dave is white. Harry is blue. Harry is white. If someone is white and kind then they are blue. If someone is white and rough then they are smart. All young, white people are blue. All white people are kind. All kind people are rough. All blue people are young.
Dave is white.
("Dave" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white and kind then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is white and rough then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All young, white people are blue.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Dave is white.
True
1
proof
[(triple1)]
("Dave" "is" "white" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is kind.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Dave" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("Dave" "is" "blue" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is smart.
True
5
proof
[(((triple3 ((((triple3) -> rule4)) -> rule5)) -> rule2))]
("Harry" "is" "smart" "+")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule5)) -> rule2))]
("Dave" "is" "smart" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is white.[(triple1)] Harry is blue.[(triple2 OR ((triple3 ((triple3) -> rule4)) -> rule1))] Harry is white.[(triple3)] @1: Dave is kind.[(((triple1) -> rule4))] Harry is kind.[(((triple3) -> rule4))] Harry is young.[(((triple2) -> rule6) OR ((((triple3 ((triple3) -> rule4)) -> rule1)) -> rule6))] @2: Dave is blue.[(((triple1 ((triple1) -> rule4)) -> rule1))] Dave is rough.[(((((triple1) -> rule4)) -> rule5))] Harry is rough.[(((((triple3) -> rule4)) -> rule5))] @3: Dave is smart.[(((triple1 ((((triple1) -> rule4)) -> rule5)) -> rule2))] Dave is young.[(((((triple1 ((triple1) -> rule4)) -> rule1)) -> rule6))] Harry is smart.[(((triple3 ((((triple3) -> rule4)) -> rule5)) -> rule2))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
((triple3 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple2) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3