Charlie is not green. Charlie is kind. Charlie is not round. Dave is furry. Dave is kind. Erin is cold. Erin is not green. Erin is not kind. Erin is young. Harry is cold. Harry is round. Harry is young. If something is big then it is round. If something is furry then it is cold. All cold things are big. If something is cold and young then it is not green. If something is furry and not round then it is young. All furry, round things are young. If something is cold and not young then it is kind. Furry, green things are kind.
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is young.
("Erin" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is cold and young then it is not green.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "-"))
If something is furry and not round then it is young.
((("something" "is" "furry" "+") ("something" "is" "round" "~")) -> ("something" "is" "young" "+"))
All furry, round things are young.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is cold and not young then it is kind.
((("something" "is" "cold" "+") ("something" "is" "young" "~")) -> ("something" "is" "kind" "+"))
Furry, green things are kind.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Erin is cold.
True
1
proof
[(triple6)]
("Erin" "is" "cold" "+")
triple6
Erin is kind.
False
1
inv-proof
[(triple8)]
("Erin" "is" "kind" "+")
triple8
Harry is big.
True
2
proof
[(((triple10) -> rule3))]
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule1))]
("Erin" "is" "round" "-")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Dave is round.
True
4
proof
[(((((((triple4) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "round" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not round.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "round" "-")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is young.
True
6
proof
[(((triple4 ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule6))]
("Dave" "is" "young" "+")
((triple4 ((((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is not young.
False
6
inv-proof
[(((triple4 ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule6))]
("Dave" "is" "young" "-")
((triple4 ((((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is not green.
True
9
proof
[(((((triple4) -> rule2) ((triple4 ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule6)) -> rule4))]
("Dave" "is" "green" "-")
((((triple4) -> (rule2 % int5)) ((triple4 ((((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
Dave is green.
False
9
inv-proof
[(((((triple4) -> rule2) ((triple4 ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule6)) -> rule4))]
("Dave" "is" "green" "+")
((((triple4) -> (rule2 % int5)) ((triple4 ((((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "kind" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Charlie is kind.[(triple2)] Charlie is not green.[(triple1)] Charlie is not round.[(triple3)] Dave is furry.[(triple4)] Dave is kind.[(triple5)] Erin is cold.[(triple6)] Erin is not green.[(triple7 OR ((triple6 triple9) -> rule4))] Erin is not kind.[(triple8)] Erin is young.[(triple9)] Harry is cold.[(triple10)] Harry is round.[(triple11 OR ((((triple10) -> rule3)) -> rule1))] Harry is young.[(triple12)] @1: Dave is cold.[(((triple4) -> rule2))] Erin is big.[(((triple6) -> rule3))] Harry is big.[(((triple10) -> rule3))] Harry is not green.[(((triple10 triple12) -> rule4))] @2: Dave is big.[(((((triple4) -> rule2)) -> rule3))] Erin is round.[(((((triple6) -> rule3)) -> rule1))] @3: Dave is round.[(((((((triple4) -> rule2)) -> rule3)) -> rule1))] @4: Dave is young.[(((triple4 ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule6))] @5: Dave is not green.[(((((triple4) -> rule2) ((triple4 ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule6)) -> rule4))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Charlie is not round.
("Charlie" "is" "round" "-")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is not green.
("Erin" "is" "green" "-")
triple7
((triple6 triple9) -> (rule4 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple6) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
((triple10 triple12) -> (rule4 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple4 ((((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is not green.
("Dave" "is" "green" "-")
((((triple4) -> (rule2 % int5)) ((triple4 ((((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5