Bob is big. Bob is cold. Bob is kind. Bob is quiet. Bob is smart. Erin is big. Erin is not cold. Erin is kind. Erin is quiet. Erin is not round. Erin is not smart. Harry is big. Harry is cold. Harry is quiet. Harry is round. Harry is smart. If something is smart then it is not white. If Erin is round and Erin is white then Erin is big. If Erin is white and Erin is round then Erin is quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not smart.
("Erin" "is" "smart" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart then it is not white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
If Erin is round and Erin is white then Erin is big.
((("Erin" "is" "round" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "big" "+"))
If Erin is white and Erin is round then Erin is quiet.
((("Erin" "is" "white" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple12)]
("Harry" "is" "big" "+")
triple12
Erin is round.
False
1
inv-proof
[(triple10)]
("Erin" "is" "round" "+")
triple10
Bob is not white.
True
2
proof
[(((triple5) -> rule1))]
("Bob" "is" "white" "-")
((triple5) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "white" "+")
((triple5) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Bob is quiet.[(triple4)] Bob is smart.[(triple5)] Erin is big.[(triple6)] Erin is kind.[(triple8)] Erin is not cold.[(triple7)] Erin is not round.[(triple10)] Erin is not smart.[(triple11)] Erin is quiet.[(triple9)] Harry is big.[(triple12)] Harry is cold.[(triple13)] Harry is quiet.[(triple14)] Harry is round.[(triple15)] Harry is smart.[(triple16)] @1: Bob is not white.[(((triple5) -> rule1))] Harry is not white.[(((triple16) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is not cold.
("Erin" "is" "cold" "-")
triple7
Erin is not round.
("Erin" "is" "round" "-")
triple10
Erin is not smart.
("Erin" "is" "smart" "-")
triple11
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Bob is not white.
("Bob" "is" "white" "-")
((triple5) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple16) -> (rule1 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1