Charlie is big. Charlie is green. Charlie is nice. Charlie is smart. Charlie is white. Charlie is young. Erin is big. Erin is not smart. Erin is white. Harry is big. Harry is not blue. Harry is green. Harry is not nice. Harry is not smart. Harry is white. Harry is young. Blue things are green. If something is smart then it is white. Blue things are white. If Charlie is big then Charlie is smart. If Harry is nice and Harry is young then Harry is white. If something is blue and not green then it is young. If something is big then it is young. All white, nice things are young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Charlie is big then Charlie is smart.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "smart" "+"))
If Harry is nice and Harry is young then Harry is white.
((("Harry" "is" "nice" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "white" "+"))
If something is blue and not green then it is young.
((("something" "is" "blue" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All white, nice things are young.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Harry is not green.
False
1
inv-proof
[(triple12)]
("Harry" "is" "green" "-")
triple12
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Charlie is nice.[(triple3)] Charlie is smart.[(triple4 OR ((triple1) -> rule4))] Charlie is white.[(triple5 OR ((triple4) -> rule2) OR ((((triple1) -> rule4)) -> rule2))] Charlie is young.[(triple6 OR ((triple1) -> rule7) OR ((triple5 triple3) -> rule8) OR ((((triple4) -> rule2) triple3) -> rule8) OR ((((((triple1) -> rule4)) -> rule2) triple3) -> rule8))] Erin is big.[(triple7)] Erin is not smart.[(triple8)] Erin is white.[(triple9)] Harry is big.[(triple10)] Harry is green.[(triple12)] Harry is not blue.[(triple11)] Harry is not nice.[(triple13)] Harry is not smart.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16 OR ((triple10) -> rule7))] @1: Erin is young.[(((triple7) -> rule7))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple1) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple4) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple1) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple4) -> (rule2 % int2)) triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is not smart.
("Erin" "is" "smart" "-")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is not blue.
("Harry" "is" "blue" "-")
triple11
Harry is not nice.
("Harry" "is" "nice" "-")
triple13
Harry is not smart.
("Harry" "is" "smart" "-")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple10) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple7) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1