Charlie is not smart. Charlie is white. Dave is cold. Dave is red. Dave is not round. Dave is smart. Erin is big. Erin is red. Erin is not round. Erin is white. Harry is not big. Harry is blue. Harry is cold. Harry is not red. Harry is round. Harry is white. If someone is big and not round then they are smart. If someone is red then they are smart. Red people are smart. Cold, white people are not smart. Smart people are not blue. If Charlie is smart then Charlie is big. Red, blue people are white. Blue, white people are cold.
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is white.
("Erin" "is" "white" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is big and not round then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "smart" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Cold, white people are not smart.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "-"))
Smart people are not blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If Charlie is smart then Charlie is big.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "big" "+"))
Red, blue people are white.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Blue, white people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Dave is red.
True
1
proof
[(triple4)]
("Dave" "is" "red" "+")
triple4
Harry is not white.
False
1
inv-proof
[(triple16)]
("Harry" "is" "white" "-")
triple16
Dave is not blue.
True
2
proof
[(((triple6) -> rule5) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule3)) -> rule5))]
("Dave" "is" "blue" "-")
((triple6) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is smart.
False
3
inv-proof
[(((triple13 triple16) -> rule4) OR ((((triple12 triple16) -> rule8) triple16) -> rule4))]
("Harry" "is" "smart" "+")
((triple13 triple16) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
((((triple12 triple16) -> (rule8 % int2)) triple16) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is not blue.
True
3
proof
[(((((triple8) -> rule2)) -> rule5) OR ((((triple8) -> rule3)) -> rule5) OR ((((triple7 triple9) -> rule1)) -> rule5))]
("Erin" "is" "blue" "-")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7 triple9) -> (rule1 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule5) OR ((((triple8) -> rule3)) -> rule5) OR ((((triple7 triple9) -> rule1)) -> rule5))]
("Erin" "is" "blue" "+")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7 triple9) -> (rule1 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "cold" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Charlie is not smart.[(triple1)] Charlie is white.[(triple2)] Dave is cold.[(triple3)] Dave is not round.[(triple5)] Dave is red.[(triple4)] Dave is smart.[(triple6 OR ((triple4) -> rule2) OR ((triple4) -> rule3))] Erin is big.[(triple7)] Erin is not round.[(triple9)] Erin is red.[(triple8)] Erin is white.[(triple10)] Harry is blue.[(triple12)] Harry is cold.[(triple13 OR ((triple12 triple16) -> rule8))] Harry is not big.[(triple11)] Harry is not red.[(triple14)] Harry is round.[(triple15)] Harry is white.[(triple16)] @1: Dave is not blue.[(((triple6) -> rule5) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule3)) -> rule5))] Erin is smart.[(((triple8) -> rule2) OR ((triple8) -> rule3) OR ((triple7 triple9) -> rule1))] Harry is not smart.[(((triple13 triple16) -> rule4) OR ((((triple12 triple16) -> rule8) triple16) -> rule4))] @2: Erin is not blue.[(((((triple8) -> rule2)) -> rule5) OR ((((triple8) -> rule3)) -> rule5) OR ((((triple7 triple9) -> rule1)) -> rule5))]
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is not round.
("Dave" "is" "round" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is not round.
("Erin" "is" "round" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple12 triple16) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
triple11
Harry is not red.
("Harry" "is" "red" "-")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Dave is not blue.
("Dave" "is" "blue" "-")
((triple6) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple8) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple7 triple9) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((triple13 triple16) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
((((triple12 triple16) -> (rule8 % int2)) triple16) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7 triple9) -> (rule1 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2