Charlie is nice. Dave is nice. Erin is green. Harry is big. Furry, young people are white. Nice people are not furry. If someone is big then they are blue. If Dave is furry then Dave is not young. Blue people are nice. If Dave is white and Dave is blue then Dave is nice.
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is green.
("Erin" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Furry, young people are white.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Nice people are not furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If Dave is furry then Dave is not young.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "young" "-"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Dave is white and Dave is blue then Dave is nice.
((("Dave" "is" "white" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "nice" "+"))
Erin is green.
True
1
proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Harry is blue.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Dave is furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Harry is nice.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("Harry" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not furry.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Harry" "is" "furry" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Harry" "is" "furry" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "blue" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Erin is nice.
Unknown
rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Erin" "is" "nice" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is nice.[(triple1)] Dave is nice.[(triple2)] Erin is green.[(triple3)] Harry is big.[(triple4)] @1: Charlie is not furry.[(((triple1) -> rule2))] Dave is not furry.[(((triple2) -> rule2))] Harry is blue.[(((triple4) -> rule3))] @2: Harry is nice.[(((((triple4) -> rule3)) -> rule5))] @3: Harry is not furry.[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3