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