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