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