Bob is big. Bob is blue. Bob is kind. Bob is nice. Bob is quiet. Charlie is kind. Charlie is round. Fiona is kind. Fiona is round. Gary is furry. Quiet, kind things are big. Quiet, big things are blue. Kind, furry things are nice. Furry things are big. If Charlie is nice and Charlie is blue then Charlie is furry. All kind things are quiet. Blue things are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Quiet, kind things are big.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Quiet, big things are blue.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Kind, furry things are nice.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Charlie is nice and Charlie is blue then Charlie is furry.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "furry" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple4 OR ((triple2) -> rule7) OR ((((triple5 triple1) -> rule2)) -> rule7) OR ((((triple5 ((triple5 triple3) -> rule1)) -> rule2)) -> rule7) OR ((((((triple3) -> rule6) triple1) -> rule2)) -> rule7) OR ((((((triple3) -> rule6) ((triple5 triple3) -> rule1)) -> rule2)) -> rule7) OR ((((triple5 ((((triple3) -> rule6) triple3) -> rule1)) -> rule2)) -> rule7) OR ((((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule1)) -> rule2)) -> rule7))]
("Bob" "is" "nice" "+")
triple4
((triple2) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple5 ((triple5 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple3) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple3) -> (rule6 % int4)) ((triple5 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((triple5 ((((triple3) -> (rule6 % int4)) triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((triple3) -> (rule6 % int4)) ((((triple3) -> (rule6 % int4)) triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Fiona is not kind.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "kind" "-")
triple8
Fiona is quiet.
True
2
proof
[(((triple8) -> rule6))]
("Fiona" "is" "quiet" "+")
((triple8) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple8) -> rule6))]
("Fiona" "is" "quiet" "-")
((triple8) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Charlie is big.
True
4
proof
[(((((triple6) -> rule6) triple6) -> rule1))]
("Charlie" "is" "big" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not big.
False
4
inv-proof
[(((((triple6) -> rule6) triple6) -> rule1))]
("Charlie" "is" "big" "-")
((((triple6) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is blue.
True
7
proof
[(((((triple8) -> rule6) ((((triple8) -> rule6) triple8) -> rule1)) -> rule2))]
("Fiona" "is" "blue" "+")
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule6 % int3)) triple8) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not blue.
False
7
inv-proof
[(((((triple8) -> rule6) ((((triple8) -> rule6) triple8) -> rule1)) -> rule2))]
("Fiona" "is" "blue" "-")
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule6 % int3)) triple8) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
True
8
proof
[(((((((triple8) -> rule6) ((((triple8) -> rule6) triple8) -> rule1)) -> rule2)) -> rule7))]
("Fiona" "is" "nice" "+")
((((((triple8) -> (rule6 % int4)) ((((triple8) -> (rule6 % int4)) triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not nice.
False
8
inv-proof
[(((((((triple8) -> rule6) ((((triple8) -> rule6) triple8) -> rule1)) -> rule2)) -> rule7))]
("Fiona" "is" "nice" "-")
((((((triple8) -> (rule6 % int4)) ((((triple8) -> (rule6 % int4)) triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Charlie is furry.
True
16
proof
[(((((((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule7) ((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule5))]
("Charlie" "is" "furry" "+")
((((((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) triple6) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) triple6) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Charlie is not furry.
False
16
inv-proof
[(((((((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule7) ((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule5))]
("Charlie" "is" "furry" "-")
((((((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) triple6) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) triple6) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Bob is big.[(triple1 OR ((triple5 triple3) -> rule1) OR ((((triple3) -> rule6) triple3) -> rule1))] Bob is blue.[(triple2 OR ((triple5 triple1) -> rule2) OR ((triple5 ((triple5 triple3) -> rule1)) -> rule2) OR ((((triple3) -> rule6) triple1) -> rule2) OR ((((triple3) -> rule6) ((triple5 triple3) -> rule1)) -> rule2) OR ((triple5 ((((triple3) -> rule6) triple3) -> rule1)) -> rule2) OR ((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule1)) -> rule2))] Bob is kind.[(triple3)] Bob is nice.[(triple4 OR ((triple2) -> rule7) OR ((((triple5 triple1) -> rule2)) -> rule7) OR ((((triple5 ((triple5 triple3) -> rule1)) -> rule2)) -> rule7) OR ((((((triple3) -> rule6) triple1) -> rule2)) -> rule7) OR ((((((triple3) -> rule6) ((triple5 triple3) -> rule1)) -> rule2)) -> rule7) OR ((((triple5 ((((triple3) -> rule6) triple3) -> rule1)) -> rule2)) -> rule7) OR ((((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule1)) -> rule2)) -> rule7))] Bob is quiet.[(triple5 OR ((triple3) -> rule6))] Charlie is kind.[(triple6)] Charlie is round.[(triple7)] Fiona is kind.[(triple8)] Fiona is round.[(triple9)] Gary is furry.[(triple10)] @1: Charlie is quiet.[(((triple6) -> rule6))] Fiona is quiet.[(((triple8) -> rule6))] Gary is big.[(((triple10) -> rule4))] @2: Charlie is big.[(((((triple6) -> rule6) triple6) -> rule1))] Fiona is big.[(((((triple8) -> rule6) triple8) -> rule1))] @3: Charlie is blue.[(((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2))] Fiona is blue.[(((((triple8) -> rule6) ((((triple8) -> rule6) triple8) -> rule1)) -> rule2))] @4: Charlie is nice.[(((((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule7))] Fiona is nice.[(((((((triple8) -> rule6) ((((triple8) -> rule6) triple8) -> rule1)) -> rule2)) -> rule7))] @5: Charlie is furry.[(((((((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule7) ((((triple6) -> rule6) ((((triple6) -> rule6) triple6) -> rule1)) -> rule2)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5 triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule6 % int2)) triple3) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5 triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5 ((triple5 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple3) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple3) -> (rule6 % int3)) ((triple5 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((triple5 ((((triple3) -> (rule6 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((triple3) -> (rule6 % int3)) ((((triple3) -> (rule6 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple2) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple5 ((triple5 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple3) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple3) -> (rule6 % int4)) ((triple5 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((triple5 ((((triple3) -> (rule6 % int4)) triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((triple3) -> (rule6 % int4)) ((((triple3) -> (rule6 % int4)) triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple8) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple10) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple6) -> (rule6 % int2)) triple6) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((triple8) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3)) triple6) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule6 % int3)) triple8) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4)) triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((triple8) -> (rule6 % int4)) ((((triple8) -> (rule6 % int4)) triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) triple6) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) triple6) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5