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