Bob is nice. Bob is round. Bob is white. Charlie is white. Dave is big. Harry is green. Harry is smart. Big things are smart. Round things are smart. White, green things are round. Kind things are white. If something is smart then it is green. All green things are kind. If Dave is smart and Dave is green then Dave is kind.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
White, green things are round.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Dave is smart and Dave is green then Dave is kind.
((("Dave" "is" "smart" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "kind" "+"))
Charlie is white.
True
1
proof
[(triple4)]
("Charlie" "is" "white" "+")
triple4
Dave is not big.
False
1
inv-proof
[(triple5)]
("Dave" "is" "big" "-")
triple5
Harry is kind.
True
2
proof
[(((triple6) -> rule6) OR ((((triple7) -> rule5)) -> rule6))]
("Harry" "is" "kind" "+")
((triple6) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is green.
True
3
proof
[(((((triple5) -> rule1)) -> rule5))]
("Dave" "is" "green" "+")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule5))]
("Dave" "is" "green" "-")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
True
4
proof
[(((((((triple5) -> rule1)) -> rule5)) -> rule6) OR ((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7))]
("Dave" "is" "kind" "+")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((((triple6) -> rule6)) -> rule4) triple6) -> rule3) OR ((((((triple6) -> rule6)) -> rule4) ((triple7) -> rule5)) -> rule3) OR ((((((((triple7) -> rule5)) -> rule6)) -> rule4) triple6) -> rule3) OR ((((((((triple7) -> rule5)) -> rule6)) -> rule4) ((triple7) -> rule5)) -> rule3))]
("Harry" "is" "round" "-")
((((((triple6) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple6) -> (rule6 % int4))) -> (rule4 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((triple7) -> (rule5 % int4))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Dave is white.
True
5
proof
[(((((((((triple5) -> rule1)) -> rule5)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7)) -> rule4))]
("Dave" "is" "white" "+")
((((((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
((((((triple5) -> (rule1 % int4)) ((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not white.
False
5
inv-proof
[(((((((((triple5) -> rule1)) -> rule5)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7)) -> rule4))]
("Dave" "is" "white" "-")
((((((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
((((((triple5) -> (rule1 % int4)) ((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is round.
True
9
proof
[(((((((((((triple5) -> rule1)) -> rule5)) -> rule6)) -> rule4) ((((triple5) -> rule1)) -> rule5)) -> rule3) OR ((((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7)) -> rule4) ((((triple5) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "round" "+")
((((((((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
((((((((triple5) -> (rule1 % int5)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is not round.
False
9
inv-proof
[(((((((((((triple5) -> rule1)) -> rule5)) -> rule6)) -> rule4) ((((triple5) -> rule1)) -> rule5)) -> rule3) OR ((((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7)) -> rule4) ((((triple5) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "round" "-")
((((((((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
((((((((triple5) -> (rule1 % int5)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Charlie is not green.
Unknown
inv-rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is round.
Unknown
rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not smart.
Unknown
inv-rconc
[@4: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is kind.
Unknown
rconc
[@4: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is nice.[(triple1)] Bob is round.[(triple2)] Bob is white.[(triple3 OR ((((((((triple2) -> rule2)) -> rule5)) -> rule6)) -> rule4))] Charlie is white.[(triple4)] Dave is big.[(triple5)] Harry is green.[(triple6 OR ((triple7) -> rule5))] Harry is smart.[(triple7 OR ((((((((triple6) -> rule6)) -> rule4) triple6) -> rule3)) -> rule2))] @1: Bob is smart.[(((triple2) -> rule2))] Dave is smart.[(((triple5) -> rule1))] Harry is kind.[(((triple6) -> rule6) OR ((((triple7) -> rule5)) -> rule6))] @2: Bob is green.[(((((triple2) -> rule2)) -> rule5))] Dave is green.[(((((triple5) -> rule1)) -> rule5))] Harry is white.[(((((triple6) -> rule6)) -> rule4) OR ((((((triple7) -> rule5)) -> rule6)) -> rule4))] @3: Bob is kind.[(((((((triple2) -> rule2)) -> rule5)) -> rule6))] Dave is kind.[(((((((triple5) -> rule1)) -> rule5)) -> rule6) OR ((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7))] Harry is round.[(((((((triple6) -> rule6)) -> rule4) triple6) -> rule3) OR ((((((triple6) -> rule6)) -> rule4) ((triple7) -> rule5)) -> rule3) OR ((((((((triple7) -> rule5)) -> rule6)) -> rule4) triple6) -> rule3) OR ((((((((triple7) -> rule5)) -> rule6)) -> rule4) ((triple7) -> rule5)) -> rule3))] @4: Dave is white.[(((((((((triple5) -> rule1)) -> rule5)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7)) -> rule4))] @5: Dave is round.[(((((((((((triple5) -> rule1)) -> rule5)) -> rule6)) -> rule4) ((((triple5) -> rule1)) -> rule5)) -> rule3) OR ((((((((triple5) -> rule1) ((((triple5) -> rule1)) -> rule5)) -> rule7)) -> rule4) ((((triple5) -> rule1)) -> rule5)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((((((((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((((((((triple6) -> (rule6 % int4))) -> (rule4 % int3)) triple6) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((((triple6) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple6) -> (rule6 % int4))) -> (rule4 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((triple7) -> (rule5 % int4))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
((((((triple5) -> (rule1 % int4)) ((((triple5) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((((((((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
((((((((triple5) -> (rule1 % int5)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5