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