Anne is green. Anne is nice. Anne is round. Charlie is young. Erin is blue. Erin is furry. Erin is smart. Erin is young. Harry is blue. Harry is furry. Harry is green. Harry is nice. If something is blue then it is young. If Erin is young and Erin is nice then Erin is furry. If Anne is furry and Anne is smart then Anne is round. If something is nice then it is round. If something is furry then it is nice. All young, nice things are round.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If Erin is young and Erin is nice then Erin is furry.
((("Erin" "is" "young" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "furry" "+"))
If Anne is furry and Anne is smart then Anne is round.
((("Anne" "is" "furry" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "round" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All young, nice things are round.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Harry is green.
True
1
proof
[(triple11)]
("Harry" "is" "green" "+")
triple11
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Harry is round.
True
2
proof
[(((triple12) -> rule4) OR ((((triple10) -> rule5)) -> rule4) OR ((((triple9) -> rule1) triple12) -> rule6) OR ((((triple9) -> rule1) ((triple10) -> rule5)) -> rule6))]
("Harry" "is" "round" "+")
((triple12) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple9) -> (rule1 % int2)) triple12) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not young.
False
2
inv-proof
[(((triple9) -> rule1))]
("Harry" "is" "young" "-")
((triple9) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Erin is round.
True
3
proof
[(((((triple6) -> rule5)) -> rule4) OR ((triple8 ((triple6) -> rule5)) -> rule6) OR ((((triple5) -> rule1) ((triple6) -> rule5)) -> rule6))]
("Erin" "is" "round" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple8 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not round.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4) OR ((triple8 ((triple6) -> rule5)) -> rule6) OR ((((triple5) -> rule1) ((triple6) -> rule5)) -> rule6))]
("Erin" "is" "round" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple8 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "nice" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2)] Anne is round.[(triple3 OR ((triple2) -> rule4))] Charlie is young.[(triple4)] Erin is blue.[(triple5)] Erin is furry.[(triple6)] Erin is smart.[(triple7)] Erin is young.[(triple8 OR ((triple5) -> rule1))] Harry is blue.[(triple9)] Harry is furry.[(triple10)] Harry is green.[(triple11)] Harry is nice.[(triple12 OR ((triple10) -> rule5))] @1: Erin is nice.[(((triple6) -> rule5))] Harry is round.[(((triple12) -> rule4) OR ((((triple10) -> rule5)) -> rule4) OR ((((triple9) -> rule1) triple12) -> rule6) OR ((((triple9) -> rule1) ((triple10) -> rule5)) -> rule6))] Harry is young.[(((triple9) -> rule1))] @2: Erin is round.[(((((triple6) -> rule5)) -> rule4) OR ((triple8 ((triple6) -> rule5)) -> rule6) OR ((((triple5) -> rule1) ((triple6) -> rule5)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
((triple5) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((triple10) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple6) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple12) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple9) -> (rule1 % int2)) triple12) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((triple9) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple8 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3