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