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