Charlie is big. Charlie is blue. Charlie is kind. Charlie is white. Fiona is kind. Fiona is smart. Fiona is white. Gary is blue. Gary is kind. Gary is smart. If Fiona is big and Fiona is white then Fiona is blue. If something is round and smart then it is blue. If Charlie is big and Charlie is round then Charlie is blue. If something is smart then it is kind. All white, blue things are kind. White things are smart. All furry things are big. If something is kind and white then it is blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Fiona is big and Fiona is white then Fiona is blue.
((("Fiona" "is" "big" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "blue" "+"))
If something is round and smart then it is blue.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If Charlie is big and Charlie is round then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "blue" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All white, blue things are kind.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is kind and white then it is blue.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple4 triple2) -> rule5) OR ((((triple4) -> rule6)) -> rule4))]
("Charlie" "is" "kind" "+")
triple3
((triple4 triple2) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Gary is not blue.
False
1
inv-proof
[(triple8)]
("Gary" "is" "blue" "-")
triple8
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2 OR ((triple3 triple4) -> rule8) OR ((((((triple4) -> rule6)) -> rule4) triple4) -> rule8))] Charlie is kind.[(triple3 OR ((triple4 triple2) -> rule5) OR ((((triple4) -> rule6)) -> rule4))] Charlie is white.[(triple4)] Fiona is kind.[(triple5 OR ((triple6) -> rule4) OR ((((triple7) -> rule6)) -> rule4))] Fiona is smart.[(triple6 OR ((triple7) -> rule6))] Fiona is white.[(triple7)] Gary is blue.[(triple8)] Gary is kind.[(triple9 OR ((triple10) -> rule4))] Gary is smart.[(triple10)] @1: Charlie is smart.[(((triple4) -> rule6))] Fiona is blue.[(((triple5 triple7) -> rule8) OR ((((triple6) -> rule4) triple7) -> rule8) OR ((((((triple7) -> rule6)) -> rule4) triple7) -> rule8))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple3 triple4) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple4 triple2) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
((triple6) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
((triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
((triple10) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple4) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5 triple7) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple6) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3