Charlie is green. Charlie is nice. Charlie is rough. Fiona is blue. Gary is kind. Gary is smart. Harry is kind. All kind things are rough. Round, nice things are blue. If something is green then it is round.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Round, nice things are blue.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Fiona is blue.
True
1
proof
[(triple4)]
("Fiona" "is" "blue" "+")
triple4
Gary is not smart.
False
1
inv-proof
[(triple6)]
("Gary" "is" "smart" "-")
triple6
Gary is rough.
True
2
proof
[(((triple5) -> rule1))]
("Gary" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "-")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
True
4
proof
[(((((triple1) -> rule3) triple2) -> rule2))]
("Charlie" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule2))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is green.[(triple1)] Charlie is nice.[(triple2)] Charlie is rough.[(triple3)] Fiona is blue.[(triple4)] Gary is kind.[(triple5)] Gary is smart.[(triple6)] Harry is kind.[(triple7)] @1: Charlie is round.[(((triple1) -> rule3))] Gary is rough.[(((triple5) -> rule1))] Harry is rough.[(((triple7) -> rule1))] @2: Charlie is blue.[(((((triple1) -> rule3) triple2) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple7) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2