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