Anne is green. Dave is not furry. Dave is smart. Dave is young. Fiona is green. Fiona is nice. Fiona is young. Harry is furry. Harry is kind. Harry is young. If something is nice then it is red. All furry, green things are young. All green things are nice. Young, smart things are kind. If Anne is furry then Anne is red. If Anne is nice and Anne is red then Anne is furry. Nice things are smart.
Anne is green.
("Anne" "is" "green" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All furry, green things are young.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Young, smart things are kind.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If Anne is furry then Anne is red.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "red" "+"))
If Anne is nice and Anne is red then Anne is furry.
((("Anne" "is" "nice" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "furry" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Harry is kind.
True
1
proof
[(triple9)]
("Harry" "is" "kind" "+")
triple9
Harry is not furry.
False
1
inv-proof
[(triple8)]
("Harry" "is" "furry" "-")
triple8
Fiona is red.
True
2
proof
[(((triple6) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("Fiona" "is" "red" "+")
((triple6) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((triple4 triple3) -> rule4))]
("Dave" "is" "kind" "-")
((triple4 triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is furry.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not furry.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
True
8
proof
[(((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6) triple1) -> rule2))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is not young.
False
8
inv-proof
[(((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6) triple1) -> rule2))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is kind.
True
12
proof
[(((((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6) triple1) -> rule2) ((((triple1) -> rule3)) -> rule7)) -> rule4))]
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule3 % int6)) ((((triple1) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule6 % int4)) triple1) -> (rule2 % int3)) ((((triple1) -> (rule3 % int6))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
int6
Anne is not kind.
False
12
inv-proof
[(((((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6) triple1) -> rule2) ((((triple1) -> rule3)) -> rule7)) -> rule4))]
("Anne" "is" "kind" "-")
((((((((triple1) -> (rule3 % int6)) ((((triple1) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule6 % int4)) triple1) -> (rule2 % int3)) ((((triple1) -> (rule3 % int6))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
int6
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "-")
Harry is smart.
Unknown
rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "red" "+")
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Anne is green.[(triple1)] Dave is not furry.[(triple2)] Dave is smart.[(triple3)] Dave is young.[(triple4)] Fiona is green.[(triple5)] Fiona is nice.[(triple6 OR ((triple5) -> rule3))] Fiona is young.[(triple7)] Harry is furry.[(triple8)] Harry is kind.[(triple9)] Harry is young.[(triple10)] @1: Anne is nice.[(((triple1) -> rule3))] Dave is kind.[(((triple4 triple3) -> rule4))] Fiona is red.[(((triple6) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] Fiona is smart.[(((triple6) -> rule7) OR ((((triple5) -> rule3)) -> rule7))] @2: Anne is red.[(((((triple1) -> rule3)) -> rule1))] Anne is smart.[(((((triple1) -> rule3)) -> rule7))] Fiona is kind.[(((triple7 ((triple6) -> rule7)) -> rule4) OR ((triple7 ((((triple5) -> rule3)) -> rule7)) -> rule4))] @3: Anne is furry.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6))] @4: Anne is young.[(((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6) triple1) -> rule2))] @5: Anne is kind.[(((((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule6) triple1) -> rule2) ((((triple1) -> rule3)) -> rule7)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
((triple5) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple4 triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple6) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple6) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple7 ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple7 ((((triple5) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule3 % int6)) ((((triple1) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule6 % int4)) triple1) -> (rule2 % int3)) ((((triple1) -> (rule3 % int6))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
int6