Anne is cold. Anne is smart. Anne is young. Charlie is blue. Charlie is cold. Charlie is smart. Charlie is white. Charlie is young. Harry is cold. Harry is kind. Harry is rough. Harry is white. All young, rough people are white. If Harry is cold then Harry is rough. If someone is smart then they are blue. If someone is kind and rough then they are smart. Cold people are smart. All cold, kind people are young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All young, rough people are white.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Harry is cold then Harry is rough.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "rough" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and rough then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All cold, kind people are young.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Charlie is young.
True
1
proof
[(triple8)]
("Charlie" "is" "young" "+")
triple8
Harry is not rough.
False
1
inv-proof
[(triple11 OR ((triple9) -> rule2))]
("Harry" "is" "rough" "-")
triple11
((triple9) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is smart.[(triple2 OR ((triple1) -> rule5))] Anne is young.[(triple3)] Charlie is blue.[(triple4 OR ((triple6) -> rule3) OR ((((triple5) -> rule5)) -> rule3))] Charlie is cold.[(triple5)] Charlie is smart.[(triple6 OR ((triple5) -> rule5))] Charlie is white.[(triple7)] Charlie is young.[(triple8)] Harry is cold.[(triple9)] Harry is kind.[(triple10)] Harry is rough.[(triple11 OR ((triple9) -> rule2))] Harry is white.[(triple12 OR ((((triple9 triple10) -> rule6) triple11) -> rule1) OR ((((triple9 triple10) -> rule6) ((triple9) -> rule2)) -> rule1))] @1: Anne is blue.[(((triple2) -> rule3) OR ((((triple1) -> rule5)) -> rule3))] Harry is smart.[(((triple9) -> rule5) OR ((triple10 triple11) -> rule4) OR ((triple10 ((triple9) -> rule2)) -> rule4))] Harry is young.[(((triple9 triple10) -> rule6))] @2: Harry is blue.[(((((triple9) -> rule5)) -> rule3) OR ((((triple10 triple11) -> rule4)) -> rule3) OR ((((triple10 ((triple9) -> rule2)) -> rule4)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple6) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple5) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple9) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple12
((((triple9 triple10) -> (rule6 % int2)) triple11) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple9 triple10) -> (rule6 % int3)) ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple9) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple10 triple11) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple10 ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple9 triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10 triple11) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10 ((triple9) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3