Dave is cold. Dave is furry. Dave is round. Dave is smart. Erin is furry. Erin is round. Erin is smart. Fiona is rough. Fiona is white. Harry is big. Harry is cold. Harry is furry. Harry is rough. Harry is round. Harry is white. If Harry is cold and Harry is smart then Harry is furry. All big things are cold. If Erin is furry then Erin is round. All big things are not smart. White things are round. Big things are round. All smart things are white. All round things are white.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is cold and Harry is smart then Harry is furry.
((("Harry" "is" "cold" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "furry" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Erin is furry then Erin is round.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "round" "+"))
All big things are not smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "-"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Harry is cold.
True
1
proof
[(triple11 OR ((triple10) -> rule2))]
("Harry" "is" "cold" "+")
triple11
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is not smart.
False
1
inv-proof
[(triple7)]
("Erin" "is" "smart" "-")
triple7
Erin is white.
True
2
proof
[(((triple6) -> rule8) OR ((triple7) -> rule7) OR ((((triple5) -> rule3)) -> rule8))]
("Erin" "is" "white" "+")
((triple6) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple7) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Harry is smart.
False
2
inv-proof
[(((triple10) -> rule4))]
("Harry" "is" "smart" "+")
((triple10) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "cold" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2)] Dave is round.[(triple3 OR ((((triple4) -> rule7)) -> rule5))] Dave is smart.[(triple4)] Erin is furry.[(triple5)] Erin is round.[(triple6 OR ((triple5) -> rule3) OR ((((triple7) -> rule7)) -> rule5))] Erin is smart.[(triple7)] Fiona is rough.[(triple8)] Fiona is white.[(triple9)] Harry is big.[(triple10)] Harry is cold.[(triple11 OR ((triple10) -> rule2))] Harry is furry.[(triple12)] Harry is rough.[(triple13)] Harry is round.[(triple14 OR ((triple10) -> rule6) OR ((triple15) -> rule5))] Harry is white.[(triple15 OR ((triple14) -> rule8) OR ((((triple10) -> rule6)) -> rule8))] @1: Dave is white.[(((triple3) -> rule8) OR ((triple4) -> rule7))] Erin is white.[(((triple6) -> rule8) OR ((triple7) -> rule7) OR ((((triple5) -> rule3)) -> rule8))] Fiona is round.[(((triple9) -> rule5))] Harry is not smart.[(((triple10) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple15) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple14) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple7) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple9) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((triple10) -> (rule4 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1